YES 8.941
H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:
↳ HASKELL
↳ LR
mainModule List
| ((group :: Eq a => [[a]] -> [[[a]]]) :: Eq a => [[a]] -> [[[a]]]) |
module List where
| import qualified Maybe import qualified Prelude
|
| group :: Eq a => [a] -> [[a]]
|
| groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
groupBy | _ [] | = | [] |
groupBy | eq (x : xs) | = |
(x : ys) : groupBy eq zs | where |
|
|
|
module Maybe where
| import qualified List import qualified Prelude
|
Lambda Reductions:
The following Lambda expression
\(_,zs)→zs
is transformed to
The following Lambda expression
\(ys,_)→ys
is transformed to
The following Lambda expression
\(_,zs)→zs
is transformed to
The following Lambda expression
\(ys,_)→ys
is transformed to
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
mainModule List
| ((group :: Eq a => [[a]] -> [[[a]]]) :: Eq a => [[a]] -> [[[a]]]) |
module List where
| import qualified Maybe import qualified Prelude
|
| group :: Eq a => [a] -> [[a]]
|
| groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
groupBy | _ [] | = | [] |
groupBy | eq (x : xs) | = |
(x : ys) : groupBy eq zs | where |
|
|
|
module Maybe where
| import qualified List import qualified Prelude
|
Replaced joker patterns by fresh variables and removed binding patterns.
Binding Reductions:
The bind variable of the following binding Pattern
xs@(ww : wx)
is replaced by the following term
ww : wx
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
mainModule List
| ((group :: Eq a => [[a]] -> [[[a]]]) :: Eq a => [[a]] -> [[[a]]]) |
module List where
| import qualified Maybe import qualified Prelude
|
| group :: Eq a => [a] -> [[a]]
|
| groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
groupBy | vw [] | = | [] |
groupBy | eq (x : xs) | = |
(x : ys) : groupBy eq zs | where |
|
|
|
module Maybe where
| import qualified List import qualified Prelude
|
Cond Reductions:
The following Function with conditions
is transformed to
undefined0 | True | = undefined |
undefined1 | | = undefined0 False |
The following Function with conditions
span | p [] | = ([],[]) |
span | p (ww : wx) | |
is transformed to
span | p [] | = span3 p [] |
span | p (ww : wx) | = span2 p (ww : wx) |
span2 | p (ww : wx) | =
span1 p ww wx (p ww) |
where |
span0 | p ww wx True | = ([],ww : wx) |
|
|
span1 | p ww wx True | = (ww : ys,zs) |
span1 | p ww wx False | = span0 p ww wx otherwise |
|
| |
| |
| |
| |
| |
|
span3 | p [] | = ([],[]) |
span3 | yz zu | = span2 yz zu |
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
mainModule List
| ((group :: Eq a => [[a]] -> [[[a]]]) :: Eq a => [[a]] -> [[[a]]]) |
module List where
| import qualified Maybe import qualified Prelude
|
| group :: Eq a => [a] -> [[a]]
|
| groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
groupBy | vw [] | = | [] |
groupBy | eq (x : xs) | = |
(x : ys) : groupBy eq zs | where |
|
|
|
module Maybe where
| import qualified List import qualified Prelude
|
Let/Where Reductions:
The bindings of the following Let/Where expression
(x : ys) : groupBy eq zs |
where | |
| |
| |
| |
| |
are unpacked to the following functions on top level
groupByVv10 | zv zw zx | = span (zv zw) zx |
groupByZs | zv zw zx | = groupByZs0 zv zw zx (groupByVv10 zv zw zx) |
groupByZs0 | zv zw zx (vy,zs) | = zs |
groupByYs0 | zv zw zx (ys,vx) | = ys |
groupByYs | zv zw zx | = groupByYs0 zv zw zx (groupByVv10 zv zw zx) |
The bindings of the following Let/Where expression
span1 p ww wx (p ww) |
where |
span0 | p ww wx True | = ([],ww : wx) |
|
|
span1 | p ww wx True | = (ww : ys,zs) |
span1 | p ww wx False | = span0 p ww wx otherwise |
|
| |
| |
| |
| |
| |
are unpacked to the following functions on top level
span2Vu43 | zy zz | = span zy zz |
span2Ys1 | zy zz (ys,wz) | = ys |
span2Zs1 | zy zz (wy,zs) | = zs |
span2Ys | zy zz | = span2Ys1 zy zz (span2Vu43 zy zz) |
span2Span0 | zy zz p ww wx True | = ([],ww : wx) |
span2Span1 | zy zz p ww wx True | = (ww : span2Ys zy zz,span2Zs zy zz) |
span2Span1 | zy zz p ww wx False | = span2Span0 zy zz p ww wx otherwise |
span2Zs | zy zz | = span2Zs1 zy zz (span2Vu43 zy zz) |
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
mainModule List
| (group :: Eq a => [[a]] -> [[[a]]]) |
module List where
| import qualified Maybe import qualified Prelude
|
| group :: Eq a => [a] -> [[a]]
|
| groupBy :: (a -> a -> Bool) -> [a] -> [[a]]
groupBy | vw [] | = | [] |
groupBy | eq (x : xs) | = | (x : groupByYs eq x xs) : groupBy eq (groupByZs eq x xs) |
|
|
groupByVv10 | zv zw zx | = | span (zv zw) zx |
|
|
groupByYs | zv zw zx | = | groupByYs0 zv zw zx (groupByVv10 zv zw zx) |
|
|
groupByYs0 | zv zw zx (ys,vx) | = | ys |
|
|
groupByZs | zv zw zx | = | groupByZs0 zv zw zx (groupByVv10 zv zw zx) |
|
|
groupByZs0 | zv zw zx (vy,zs) | = | zs |
|
module Maybe where
| import qualified List import qualified Prelude
|
Haskell To QDPs
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primPlusNat(Succ(vuu4900), Succ(vuu31000000)) → new_primPlusNat(vuu4900, vuu31000000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primPlusNat(Succ(vuu4900), Succ(vuu31000000)) → new_primPlusNat(vuu4900, vuu31000000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primMulNat(Succ(vuu300000), Succ(vuu3100000)) → new_primMulNat(vuu300000, Succ(vuu3100000))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primMulNat(Succ(vuu300000), Succ(vuu3100000)) → new_primMulNat(vuu300000, Succ(vuu3100000))
The graph contains the following edges 1 > 1, 2 >= 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_primEqNat(Succ(vuu30000), Succ(vuu310000)) → new_primEqNat(vuu30000, vuu310000)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_primEqNat(Succ(vuu30000), Succ(vuu310000)) → new_primEqNat(vuu30000, vuu310000)
The graph contains the following edges 1 > 1, 2 > 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_esEs2(Just(vuu3000), Just(vuu31000), app(app(app(ty_@3, bbb), bbc), bbd)) → new_esEs1(vuu3000, vuu31000, bbb, bbc, bbd)
new_esEs0(:(vuu3000, vuu3001), :(vuu31000, vuu31001), app(app(ty_@2, ee), ef)) → new_esEs3(vuu3000, vuu31000, ee, ef)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), gd, app(app(ty_@2, hd), he), fc) → new_esEs3(vuu3001, vuu31001, hd, he)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), gd, app(app(app(ty_@3, gh), ha), hb), fc) → new_esEs1(vuu3001, vuu31001, gh, ha, hb)
new_esEs3(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), bdb, app(ty_Maybe, bea)) → new_esEs2(vuu3001, vuu31001, bea)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), app(ty_[], fd), fb, fc) → new_esEs0(vuu3000, vuu31000, fd)
new_esEs2(Just(vuu3000), Just(vuu31000), app(app(ty_Either, bag), bah)) → new_esEs(vuu3000, vuu31000, bag, bah)
new_esEs(Right(vuu3000), Right(vuu31000), cc, app(app(ty_@2, dd), de)) → new_esEs3(vuu3000, vuu31000, dd, de)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), gd, fb, app(app(app(ty_@3, baa), bab), bac)) → new_esEs1(vuu3002, vuu31002, baa, bab, bac)
new_esEs2(Just(vuu3000), Just(vuu31000), app(ty_Maybe, bbe)) → new_esEs2(vuu3000, vuu31000, bbe)
new_esEs(Left(vuu3000), Left(vuu31000), app(ty_Maybe, bh), bc) → new_esEs2(vuu3000, vuu31000, bh)
new_esEs3(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), app(app(app(ty_@3, bcd), bce), bcf), bcb) → new_esEs1(vuu3000, vuu31000, bcd, bce, bcf)
new_esEs3(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), bdb, app(app(ty_@2, beb), bec)) → new_esEs3(vuu3001, vuu31001, beb, bec)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), gd, fb, app(ty_[], hh)) → new_esEs0(vuu3002, vuu31002, hh)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), app(app(app(ty_@3, ff), fg), fh), fb, fc) → new_esEs1(vuu3000, vuu31000, ff, fg, fh)
new_esEs(Right(vuu3000), Right(vuu31000), cc, app(app(app(ty_@3, cg), da), db)) → new_esEs1(vuu3000, vuu31000, cg, da, db)
new_esEs(Right(vuu3000), Right(vuu31000), cc, app(app(ty_Either, cd), ce)) → new_esEs(vuu3000, vuu31000, cd, ce)
new_esEs3(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), app(ty_Maybe, bcg), bcb) → new_esEs2(vuu3000, vuu31000, bcg)
new_esEs(Left(vuu3000), Left(vuu31000), app(app(ty_@2, ca), cb), bc) → new_esEs3(vuu3000, vuu31000, ca, cb)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), gd, app(ty_Maybe, hc), fc) → new_esEs2(vuu3001, vuu31001, hc)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), app(app(ty_@2, gb), gc), fb, fc) → new_esEs3(vuu3000, vuu31000, gb, gc)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), gd, fb, app(app(ty_Either, hf), hg)) → new_esEs(vuu3002, vuu31002, hf, hg)
new_esEs0(:(vuu3000, vuu3001), :(vuu31000, vuu31001), app(app(app(ty_@3, ea), eb), ec)) → new_esEs1(vuu3000, vuu31000, ea, eb, ec)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), gd, app(ty_[], gg), fc) → new_esEs0(vuu3001, vuu31001, gg)
new_esEs2(Just(vuu3000), Just(vuu31000), app(ty_[], bba)) → new_esEs0(vuu3000, vuu31000, bba)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), gd, fb, app(ty_Maybe, bad)) → new_esEs2(vuu3002, vuu31002, bad)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), gd, app(app(ty_Either, ge), gf), fc) → new_esEs(vuu3001, vuu31001, ge, gf)
new_esEs3(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), app(app(ty_@2, bch), bda), bcb) → new_esEs3(vuu3000, vuu31000, bch, bda)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), app(app(ty_Either, eh), fa), fb, fc) → new_esEs(vuu3000, vuu31000, eh, fa)
new_esEs(Right(vuu3000), Right(vuu31000), cc, app(ty_Maybe, dc)) → new_esEs2(vuu3000, vuu31000, dc)
new_esEs3(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), bdb, app(ty_[], bde)) → new_esEs0(vuu3001, vuu31001, bde)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), app(ty_Maybe, ga), fb, fc) → new_esEs2(vuu3000, vuu31000, ga)
new_esEs0(:(vuu3000, vuu3001), :(vuu31000, vuu31001), app(ty_Maybe, ed)) → new_esEs2(vuu3000, vuu31000, ed)
new_esEs0(:(vuu3000, vuu3001), :(vuu31000, vuu31001), app(app(ty_Either, df), dg)) → new_esEs(vuu3000, vuu31000, df, dg)
new_esEs3(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), bdb, app(app(ty_Either, bdc), bdd)) → new_esEs(vuu3001, vuu31001, bdc, bdd)
new_esEs(Left(vuu3000), Left(vuu31000), app(app(app(ty_@3, be), bf), bg), bc) → new_esEs1(vuu3000, vuu31000, be, bf, bg)
new_esEs2(Just(vuu3000), Just(vuu31000), app(app(ty_@2, bbf), bbg)) → new_esEs3(vuu3000, vuu31000, bbf, bbg)
new_esEs3(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), app(app(ty_Either, bbh), bca), bcb) → new_esEs(vuu3000, vuu31000, bbh, bca)
new_esEs(Left(vuu3000), Left(vuu31000), app(ty_[], bd), bc) → new_esEs0(vuu3000, vuu31000, bd)
new_esEs3(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), bdb, app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs1(vuu3001, vuu31001, bdf, bdg, bdh)
new_esEs0(:(vuu3000, vuu3001), :(vuu31000, vuu31001), app(ty_[], dh)) → new_esEs0(vuu3000, vuu31000, dh)
new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), gd, fb, app(app(ty_@2, bae), baf)) → new_esEs3(vuu3002, vuu31002, bae, baf)
new_esEs3(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), app(ty_[], bcc), bcb) → new_esEs0(vuu3000, vuu31000, bcc)
new_esEs(Right(vuu3000), Right(vuu31000), cc, app(ty_[], cf)) → new_esEs0(vuu3000, vuu31000, cf)
new_esEs0(:(vuu3000, vuu3001), :(vuu31000, vuu31001), eg) → new_esEs0(vuu3001, vuu31001, eg)
new_esEs(Left(vuu3000), Left(vuu31000), app(app(ty_Either, ba), bb), bc) → new_esEs(vuu3000, vuu31000, ba, bb)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_esEs2(Just(vuu3000), Just(vuu31000), app(ty_Maybe, bbe)) → new_esEs2(vuu3000, vuu31000, bbe)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Just(vuu3000), Just(vuu31000), app(app(app(ty_@3, bbb), bbc), bbd)) → new_esEs1(vuu3000, vuu31000, bbb, bbc, bbd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs2(Just(vuu3000), Just(vuu31000), app(ty_[], bba)) → new_esEs0(vuu3000, vuu31000, bba)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs2(Just(vuu3000), Just(vuu31000), app(app(ty_@2, bbf), bbg)) → new_esEs3(vuu3000, vuu31000, bbf, bbg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs2(Just(vuu3000), Just(vuu31000), app(app(ty_Either, bag), bah)) → new_esEs(vuu3000, vuu31000, bag, bah)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(vuu3000, vuu3001), :(vuu31000, vuu31001), app(ty_Maybe, ed)) → new_esEs2(vuu3000, vuu31000, ed)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(vuu3000, vuu3001), :(vuu31000, vuu31001), app(app(app(ty_@3, ea), eb), ec)) → new_esEs1(vuu3000, vuu31000, ea, eb, ec)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(:(vuu3000, vuu3001), :(vuu31000, vuu31001), app(app(ty_@2, ee), ef)) → new_esEs3(vuu3000, vuu31000, ee, ef)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs0(:(vuu3000, vuu3001), :(vuu31000, vuu31001), app(app(ty_Either, df), dg)) → new_esEs(vuu3000, vuu31000, df, dg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), gd, app(ty_Maybe, hc), fc) → new_esEs2(vuu3001, vuu31001, hc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), gd, fb, app(ty_Maybe, bad)) → new_esEs2(vuu3002, vuu31002, bad)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), app(ty_Maybe, ga), fb, fc) → new_esEs2(vuu3000, vuu31000, ga)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), gd, app(app(app(ty_@3, gh), ha), hb), fc) → new_esEs1(vuu3001, vuu31001, gh, ha, hb)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), gd, fb, app(app(app(ty_@3, baa), bab), bac)) → new_esEs1(vuu3002, vuu31002, baa, bab, bac)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4, 5 > 5
- new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), app(app(app(ty_@3, ff), fg), fh), fb, fc) → new_esEs1(vuu3000, vuu31000, ff, fg, fh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), app(ty_[], fd), fb, fc) → new_esEs0(vuu3000, vuu31000, fd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), gd, fb, app(ty_[], hh)) → new_esEs0(vuu3002, vuu31002, hh)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3
- new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), gd, app(ty_[], gg), fc) → new_esEs0(vuu3001, vuu31001, gg)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), gd, app(app(ty_@2, hd), he), fc) → new_esEs3(vuu3001, vuu31001, hd, he)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), app(app(ty_@2, gb), gc), fb, fc) → new_esEs3(vuu3000, vuu31000, gb, gc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), gd, fb, app(app(ty_@2, bae), baf)) → new_esEs3(vuu3002, vuu31002, bae, baf)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), gd, fb, app(app(ty_Either, hf), hg)) → new_esEs(vuu3002, vuu31002, hf, hg)
The graph contains the following edges 1 > 1, 2 > 2, 5 > 3, 5 > 4
- new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), gd, app(app(ty_Either, ge), gf), fc) → new_esEs(vuu3001, vuu31001, ge, gf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs1(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), app(app(ty_Either, eh), fa), fb, fc) → new_esEs(vuu3000, vuu31000, eh, fa)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), bdb, app(ty_Maybe, bea)) → new_esEs2(vuu3001, vuu31001, bea)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), app(ty_Maybe, bcg), bcb) → new_esEs2(vuu3000, vuu31000, bcg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(Left(vuu3000), Left(vuu31000), app(ty_Maybe, bh), bc) → new_esEs2(vuu3000, vuu31000, bh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(Right(vuu3000), Right(vuu31000), cc, app(ty_Maybe, dc)) → new_esEs2(vuu3000, vuu31000, dc)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), app(app(app(ty_@3, bcd), bce), bcf), bcb) → new_esEs1(vuu3000, vuu31000, bcd, bce, bcf)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs3(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), bdb, app(app(app(ty_@3, bdf), bdg), bdh)) → new_esEs1(vuu3001, vuu31001, bdf, bdg, bdh)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs3(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), bdb, app(ty_[], bde)) → new_esEs0(vuu3001, vuu31001, bde)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs3(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), app(ty_[], bcc), bcb) → new_esEs0(vuu3000, vuu31000, bcc)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs3(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), bdb, app(app(ty_@2, beb), bec)) → new_esEs3(vuu3001, vuu31001, beb, bec)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), app(app(ty_@2, bch), bda), bcb) → new_esEs3(vuu3000, vuu31000, bch, bda)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs3(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), bdb, app(app(ty_Either, bdc), bdd)) → new_esEs(vuu3001, vuu31001, bdc, bdd)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs3(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), app(app(ty_Either, bbh), bca), bcb) → new_esEs(vuu3000, vuu31000, bbh, bca)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(Right(vuu3000), Right(vuu31000), cc, app(app(app(ty_@3, cg), da), db)) → new_esEs1(vuu3000, vuu31000, cg, da, db)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4, 4 > 5
- new_esEs(Left(vuu3000), Left(vuu31000), app(app(app(ty_@3, be), bf), bg), bc) → new_esEs1(vuu3000, vuu31000, be, bf, bg)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4, 3 > 5
- new_esEs0(:(vuu3000, vuu3001), :(vuu31000, vuu31001), app(ty_[], dh)) → new_esEs0(vuu3000, vuu31000, dh)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs0(:(vuu3000, vuu3001), :(vuu31000, vuu31001), eg) → new_esEs0(vuu3001, vuu31001, eg)
The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3
- new_esEs(Left(vuu3000), Left(vuu31000), app(ty_[], bd), bc) → new_esEs0(vuu3000, vuu31000, bd)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3
- new_esEs(Right(vuu3000), Right(vuu31000), cc, app(ty_[], cf)) → new_esEs0(vuu3000, vuu31000, cf)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3
- new_esEs(Right(vuu3000), Right(vuu31000), cc, app(app(ty_@2, dd), de)) → new_esEs3(vuu3000, vuu31000, dd, de)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(Left(vuu3000), Left(vuu31000), app(app(ty_@2, ca), cb), bc) → new_esEs3(vuu3000, vuu31000, ca, cb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
- new_esEs(Right(vuu3000), Right(vuu31000), cc, app(app(ty_Either, cd), ce)) → new_esEs(vuu3000, vuu31000, cd, ce)
The graph contains the following edges 1 > 1, 2 > 2, 4 > 3, 4 > 4
- new_esEs(Left(vuu3000), Left(vuu31000), app(app(ty_Either, ba), bb), bc) → new_esEs(vuu3000, vuu31000, ba, bb)
The graph contains the following edges 1 > 1, 2 > 2, 3 > 3, 3 > 4
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_span2Zs1(vuu3110, vuu3111, True, ba) → new_span2Zs(vuu3111, ba)
new_span2Zs(:(vuu3110, vuu3111), ba) → new_span2Zs1(vuu3110, vuu3111, new_esEs4([], vuu3110, ba), ba)
new_span2Ys1(vuu3110, vuu3111, True, ba) → new_span2Zs(vuu3111, ba)
new_span2Ys1(vuu3110, vuu3111, True, ba) → new_span2Ys(vuu3111, ba)
new_span2Ys(:(vuu3110, vuu3111), ba) → new_span2Ys1(vuu3110, vuu3111, new_esEs4([], vuu3110, ba), ba)
new_span2Zs1(vuu3110, vuu3111, True, ba) → new_span2Ys(vuu3111, ba)
The TRS R consists of the following rules:
new_esEs22(vuu3002, vuu31002, app(app(ty_@2, bbd), bbe)) → new_esEs15(vuu3002, vuu31002, bbd, bbe)
new_esEs8(Right(vuu3000), Right(vuu31000), bee, ty_Double) → new_esEs14(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, ty_Char) → new_esEs6(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, app(ty_Ratio, fh)) → new_esEs7(vuu3000, vuu31000, fh)
new_esEs8(Right(vuu3000), Right(vuu31000), bee, app(ty_[], bfa)) → new_esEs4(vuu3000, vuu31000, bfa)
new_primPlusNat1(Succ(vuu4900), Succ(vuu31000000)) → Succ(Succ(new_primPlusNat1(vuu4900, vuu31000000)))
new_esEs19(vuu3001, vuu31001, app(ty_Ratio, eb)) → new_esEs7(vuu3001, vuu31001, eb)
new_primEqInt(Neg(Succ(vuu30000)), Pos(vuu31000)) → False
new_primEqInt(Pos(Succ(vuu30000)), Neg(vuu31000)) → False
new_esEs18(vuu3000, vuu31000, ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs19(vuu3001, vuu31001, ty_Bool) → new_esEs11(vuu3001, vuu31001)
new_esEs8(Left(vuu3000), Left(vuu31000), app(ty_[], bdf), bdb) → new_esEs4(vuu3000, vuu31000, bdf)
new_primEqInt(Neg(Zero), Pos(Succ(vuu310000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(vuu310000))) → False
new_esEs8(Right(vuu3000), Right(vuu31000), bee, ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, ty_Int) → new_esEs9(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, ty_Bool) → new_esEs11(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, app(app(ty_@2, gh), ha)) → new_esEs15(vuu3000, vuu31000, gh, ha)
new_esEs23(vuu3000, vuu31000, ty_Float) → new_esEs17(vuu3000, vuu31000)
new_esEs19(vuu3001, vuu31001, ty_Ordering) → new_esEs13(vuu3001, vuu31001)
new_primMulNat0(Zero, Zero) → Zero
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Double) → new_esEs14(vuu3000, vuu31000)
new_esEs15(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), ce, cf) → new_asAs(new_esEs18(vuu3000, vuu31000, ce), new_esEs19(vuu3001, vuu31001, cf))
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Int) → new_esEs9(vuu3000, vuu31000)
new_esEs21(vuu3001, vuu31001, app(app(ty_Either, hc), hd)) → new_esEs8(vuu3001, vuu31001, hc, hd)
new_esEs23(vuu3000, vuu31000, app(app(app(ty_@3, bcc), bcd), bce)) → new_esEs12(vuu3000, vuu31000, bcc, bcd, bce)
new_primPlusNat0(Zero, vuu3100000) → Succ(vuu3100000)
new_esEs21(vuu3001, vuu31001, app(app(ty_@2, bab), bac)) → new_esEs15(vuu3001, vuu31001, bab, bac)
new_esEs20(vuu3000, vuu31000, app(app(app(ty_@3, gd), ge), gf)) → new_esEs12(vuu3000, vuu31000, gd, ge, gf)
new_esEs13(EQ, EQ) → True
new_esEs12(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), fd, ff, fg) → new_asAs(new_esEs20(vuu3000, vuu31000, fd), new_asAs(new_esEs21(vuu3001, vuu31001, ff), new_esEs22(vuu3002, vuu31002, fg)))
new_sr(Neg(vuu30000), Pos(vuu310000)) → Neg(new_primMulNat0(vuu30000, vuu310000))
new_sr(Pos(vuu30000), Neg(vuu310000)) → Neg(new_primMulNat0(vuu30000, vuu310000))
new_esEs19(vuu3001, vuu31001, ty_Int) → new_esEs9(vuu3001, vuu31001)
new_esEs23(vuu3000, vuu31000, ty_@0) → new_esEs10(vuu3000, vuu31000)
new_esEs4(:(vuu3000, vuu3001), :(vuu31000, vuu31001), bbf) → new_asAs(new_esEs23(vuu3000, vuu31000, bbf), new_esEs4(vuu3001, vuu31001, bbf))
new_esEs22(vuu3002, vuu31002, ty_Bool) → new_esEs11(vuu3002, vuu31002)
new_esEs19(vuu3001, vuu31001, app(app(app(ty_@3, ef), eg), eh)) → new_esEs12(vuu3001, vuu31001, ef, eg, eh)
new_esEs21(vuu3001, vuu31001, ty_Integer) → new_esEs16(vuu3001, vuu31001)
new_esEs18(vuu3000, vuu31000, ty_Ordering) → new_esEs13(vuu3000, vuu31000)
new_esEs5(Just(vuu3000), Just(vuu31000), app(ty_Maybe, cb)) → new_esEs5(vuu3000, vuu31000, cb)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Float, bdb) → new_esEs17(vuu3000, vuu31000)
new_esEs24(vuu3000, vuu31000, ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs18(vuu3000, vuu31000, ty_Int) → new_esEs9(vuu3000, vuu31000)
new_esEs18(vuu3000, vuu31000, ty_Char) → new_esEs6(vuu3000, vuu31000)
new_esEs8(Right(vuu3000), Right(vuu31000), bee, ty_@0) → new_esEs10(vuu3000, vuu31000)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Double, bdb) → new_esEs14(vuu3000, vuu31000)
new_esEs13(GT, GT) → True
new_esEs8(Right(vuu3000), Right(vuu31000), bee, ty_Ordering) → new_esEs13(vuu3000, vuu31000)
new_primEqNat0(Zero, Succ(vuu310000)) → False
new_primEqNat0(Succ(vuu30000), Zero) → False
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Int, bdb) → new_esEs9(vuu3000, vuu31000)
new_esEs22(vuu3002, vuu31002, ty_Float) → new_esEs17(vuu3002, vuu31002)
new_esEs21(vuu3001, vuu31001, ty_Int) → new_esEs9(vuu3001, vuu31001)
new_esEs21(vuu3001, vuu31001, ty_@0) → new_esEs10(vuu3001, vuu31001)
new_esEs19(vuu3001, vuu31001, app(app(ty_@2, fb), fc)) → new_esEs15(vuu3001, vuu31001, fb, fc)
new_esEs22(vuu3002, vuu31002, ty_Char) → new_esEs6(vuu3002, vuu31002)
new_esEs17(Float(vuu3000, vuu3001), Float(vuu31000, vuu31001)) → new_esEs9(new_sr(vuu3000, vuu31000), new_sr(vuu3001, vuu31001))
new_esEs5(Just(vuu3000), Just(vuu31000), app(ty_Ratio, bc)) → new_esEs7(vuu3000, vuu31000, bc)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs22(vuu3002, vuu31002, ty_Double) → new_esEs14(vuu3002, vuu31002)
new_esEs13(EQ, LT) → False
new_esEs13(LT, EQ) → False
new_esEs20(vuu3000, vuu31000, ty_Ordering) → new_esEs13(vuu3000, vuu31000)
new_esEs14(Double(vuu3000, vuu3001), Double(vuu31000, vuu31001)) → new_esEs9(new_sr(vuu3000, vuu31000), new_sr(vuu3001, vuu31001))
new_esEs19(vuu3001, vuu31001, app(app(ty_Either, ec), ed)) → new_esEs8(vuu3001, vuu31001, ec, ed)
new_esEs22(vuu3002, vuu31002, ty_Ordering) → new_esEs13(vuu3002, vuu31002)
new_esEs22(vuu3002, vuu31002, ty_Int) → new_esEs9(vuu3002, vuu31002)
new_esEs18(vuu3000, vuu31000, app(app(app(ty_@3, dd), de), df)) → new_esEs12(vuu3000, vuu31000, dd, de, df)
new_esEs20(vuu3000, vuu31000, app(ty_[], gc)) → new_esEs4(vuu3000, vuu31000, gc)
new_esEs21(vuu3001, vuu31001, ty_Ordering) → new_esEs13(vuu3001, vuu31001)
new_esEs22(vuu3002, vuu31002, app(app(app(ty_@3, bah), bba), bbb)) → new_esEs12(vuu3002, vuu31002, bah, bba, bbb)
new_esEs19(vuu3001, vuu31001, app(ty_Maybe, fa)) → new_esEs5(vuu3001, vuu31001, fa)
new_esEs21(vuu3001, vuu31001, app(app(app(ty_@3, hf), hg), hh)) → new_esEs12(vuu3001, vuu31001, hf, hg, hh)
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Ordering) → new_esEs13(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, app(app(ty_Either, bbh), bca)) → new_esEs8(vuu3000, vuu31000, bbh, bca)
new_esEs22(vuu3002, vuu31002, ty_@0) → new_esEs10(vuu3002, vuu31002)
new_esEs24(vuu3000, vuu31000, ty_Int) → new_esEs9(vuu3000, vuu31000)
new_esEs25(vuu3001, vuu31001, ty_Integer) → new_esEs16(vuu3001, vuu31001)
new_esEs5(Just(vuu3000), Just(vuu31000), app(app(app(ty_@3, bg), bh), ca)) → new_esEs12(vuu3000, vuu31000, bg, bh, ca)
new_esEs18(vuu3000, vuu31000, app(app(ty_Either, da), db)) → new_esEs8(vuu3000, vuu31000, da, db)
new_esEs11(False, True) → False
new_esEs11(True, False) → False
new_esEs19(vuu3001, vuu31001, ty_Double) → new_esEs14(vuu3001, vuu31001)
new_esEs18(vuu3000, vuu31000, app(app(ty_@2, dh), ea)) → new_esEs15(vuu3000, vuu31000, dh, ea)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Char, bdb) → new_esEs6(vuu3000, vuu31000)
new_esEs8(Right(vuu3000), Right(vuu31000), bee, app(app(ty_@2, bff), bfg)) → new_esEs15(vuu3000, vuu31000, bff, bfg)
new_esEs23(vuu3000, vuu31000, ty_Double) → new_esEs14(vuu3000, vuu31000)
new_esEs16(Integer(vuu3000), Integer(vuu31000)) → new_primEqInt(vuu3000, vuu31000)
new_esEs8(Left(vuu3000), Left(vuu31000), app(app(ty_Either, bdd), bde), bdb) → new_esEs8(vuu3000, vuu31000, bdd, bde)
new_esEs8(Right(vuu3000), Right(vuu31000), bee, app(app(app(ty_@3, bfb), bfc), bfd)) → new_esEs12(vuu3000, vuu31000, bfb, bfc, bfd)
new_esEs21(vuu3001, vuu31001, ty_Bool) → new_esEs11(vuu3001, vuu31001)
new_esEs20(vuu3000, vuu31000, ty_Char) → new_esEs6(vuu3000, vuu31000)
new_esEs19(vuu3001, vuu31001, ty_Float) → new_esEs17(vuu3001, vuu31001)
new_esEs10(@0, @0) → True
new_esEs22(vuu3002, vuu31002, app(ty_Ratio, bad)) → new_esEs7(vuu3002, vuu31002, bad)
new_sr(Neg(vuu30000), Neg(vuu310000)) → Pos(new_primMulNat0(vuu30000, vuu310000))
new_esEs20(vuu3000, vuu31000, ty_Bool) → new_esEs11(vuu3000, vuu31000)
new_esEs21(vuu3001, vuu31001, app(ty_[], he)) → new_esEs4(vuu3001, vuu31001, he)
new_esEs20(vuu3000, vuu31000, app(ty_Maybe, gg)) → new_esEs5(vuu3000, vuu31000, gg)
new_esEs5(Just(vuu3000), Just(vuu31000), app(ty_[], bf)) → new_esEs4(vuu3000, vuu31000, bf)
new_asAs(False, vuu37) → False
new_sr(Pos(vuu30000), Pos(vuu310000)) → Pos(new_primMulNat0(vuu30000, vuu310000))
new_esEs7(:%(vuu3000, vuu3001), :%(vuu31000, vuu31001), bda) → new_asAs(new_esEs24(vuu3000, vuu31000, bda), new_esEs25(vuu3001, vuu31001, bda))
new_primEqNat0(Zero, Zero) → True
new_primMulNat0(Zero, Succ(vuu3100000)) → Zero
new_primMulNat0(Succ(vuu300000), Zero) → Zero
new_esEs13(GT, EQ) → False
new_esEs13(EQ, GT) → False
new_esEs13(GT, LT) → False
new_esEs13(LT, GT) → False
new_esEs23(vuu3000, vuu31000, ty_Int) → new_esEs9(vuu3000, vuu31000)
new_esEs18(vuu3000, vuu31000, app(ty_Maybe, dg)) → new_esEs5(vuu3000, vuu31000, dg)
new_esEs18(vuu3000, vuu31000, app(ty_[], dc)) → new_esEs4(vuu3000, vuu31000, dc)
new_esEs8(Right(vuu3000), Right(vuu31000), bee, app(ty_Maybe, bfe)) → new_esEs5(vuu3000, vuu31000, bfe)
new_esEs11(True, True) → True
new_esEs23(vuu3000, vuu31000, app(ty_Maybe, bcf)) → new_esEs5(vuu3000, vuu31000, bcf)
new_esEs8(Left(vuu3000), Left(vuu31000), app(ty_Ratio, bdc), bdb) → new_esEs7(vuu3000, vuu31000, bdc)
new_esEs5(Just(vuu3000), Just(vuu31000), app(app(ty_@2, cc), cd)) → new_esEs15(vuu3000, vuu31000, cc, cd)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Ordering, bdb) → new_esEs13(vuu3000, vuu31000)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Bool, bdb) → new_esEs11(vuu3000, vuu31000)
new_primPlusNat0(Succ(vuu490), vuu3100000) → Succ(Succ(new_primPlusNat1(vuu490, vuu3100000)))
new_esEs8(Left(vuu3000), Left(vuu31000), app(app(ty_@2, bec), bed), bdb) → new_esEs15(vuu3000, vuu31000, bec, bed)
new_esEs5(Just(vuu3000), Just(vuu31000), app(app(ty_Either, bd), be)) → new_esEs8(vuu3000, vuu31000, bd, be)
new_esEs5(Just(vuu3000), Nothing, bb) → False
new_esEs5(Nothing, Just(vuu31000), bb) → False
new_esEs19(vuu3001, vuu31001, ty_Integer) → new_esEs16(vuu3001, vuu31001)
new_esEs19(vuu3001, vuu31001, ty_Char) → new_esEs6(vuu3001, vuu31001)
new_primEqInt(Neg(Succ(vuu30000)), Neg(Succ(vuu310000))) → new_primEqNat0(vuu30000, vuu310000)
new_esEs4([], [], bbf) → True
new_esEs20(vuu3000, vuu31000, ty_Float) → new_esEs17(vuu3000, vuu31000)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_@0, bdb) → new_esEs10(vuu3000, vuu31000)
new_esEs18(vuu3000, vuu31000, ty_@0) → new_esEs10(vuu3000, vuu31000)
new_primPlusNat1(Succ(vuu4900), Zero) → Succ(vuu4900)
new_primPlusNat1(Zero, Succ(vuu31000000)) → Succ(vuu31000000)
new_esEs23(vuu3000, vuu31000, app(ty_Ratio, bbg)) → new_esEs7(vuu3000, vuu31000, bbg)
new_esEs8(Right(vuu3000), Right(vuu31000), bee, app(app(ty_Either, beg), beh)) → new_esEs8(vuu3000, vuu31000, beg, beh)
new_esEs8(Right(vuu3000), Left(vuu31000), bee, bdb) → False
new_esEs8(Left(vuu3000), Right(vuu31000), bee, bdb) → False
new_esEs18(vuu3000, vuu31000, app(ty_Ratio, cg)) → new_esEs7(vuu3000, vuu31000, cg)
new_esEs6(Char(vuu3000), Char(vuu31000)) → new_primEqNat0(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, app(app(ty_Either, ga), gb)) → new_esEs8(vuu3000, vuu31000, ga, gb)
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Float) → new_esEs17(vuu3000, vuu31000)
new_esEs21(vuu3001, vuu31001, ty_Double) → new_esEs14(vuu3001, vuu31001)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs18(vuu3000, vuu31000, ty_Float) → new_esEs17(vuu3000, vuu31000)
new_esEs5(Nothing, Nothing, bb) → True
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs18(vuu3000, vuu31000, ty_Bool) → new_esEs11(vuu3000, vuu31000)
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Char) → new_esEs6(vuu3000, vuu31000)
new_esEs22(vuu3002, vuu31002, ty_Integer) → new_esEs16(vuu3002, vuu31002)
new_primEqInt(Neg(Zero), Neg(Succ(vuu310000))) → False
new_primEqInt(Neg(Succ(vuu30000)), Neg(Zero)) → False
new_esEs23(vuu3000, vuu31000, ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs4([], :(vuu31000, vuu31001), bbf) → False
new_esEs4(:(vuu3000, vuu3001), [], bbf) → False
new_esEs20(vuu3000, vuu31000, ty_@0) → new_esEs10(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs22(vuu3002, vuu31002, app(ty_Maybe, bbc)) → new_esEs5(vuu3002, vuu31002, bbc)
new_esEs21(vuu3001, vuu31001, app(ty_Maybe, baa)) → new_esEs5(vuu3001, vuu31001, baa)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs21(vuu3001, vuu31001, ty_Float) → new_esEs17(vuu3001, vuu31001)
new_asAs(True, vuu37) → vuu37
new_esEs5(Just(vuu3000), Just(vuu31000), ty_@0) → new_esEs10(vuu3000, vuu31000)
new_primMulNat0(Succ(vuu300000), Succ(vuu3100000)) → new_primPlusNat0(new_primMulNat0(vuu300000, Succ(vuu3100000)), vuu3100000)
new_esEs19(vuu3001, vuu31001, app(ty_[], ee)) → new_esEs4(vuu3001, vuu31001, ee)
new_esEs8(Right(vuu3000), Right(vuu31000), bee, ty_Int) → new_esEs9(vuu3000, vuu31000)
new_esEs13(LT, LT) → True
new_esEs18(vuu3000, vuu31000, ty_Double) → new_esEs14(vuu3000, vuu31000)
new_esEs22(vuu3002, vuu31002, app(ty_[], bag)) → new_esEs4(vuu3002, vuu31002, bag)
new_esEs11(False, False) → True
new_primEqInt(Pos(Succ(vuu30000)), Pos(Succ(vuu310000))) → new_primEqNat0(vuu30000, vuu310000)
new_esEs8(Right(vuu3000), Right(vuu31000), bee, ty_Char) → new_esEs6(vuu3000, vuu31000)
new_esEs8(Right(vuu3000), Right(vuu31000), bee, ty_Float) → new_esEs17(vuu3000, vuu31000)
new_esEs19(vuu3001, vuu31001, ty_@0) → new_esEs10(vuu3001, vuu31001)
new_esEs22(vuu3002, vuu31002, app(app(ty_Either, bae), baf)) → new_esEs8(vuu3002, vuu31002, bae, baf)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Integer, bdb) → new_esEs16(vuu3000, vuu31000)
new_esEs25(vuu3001, vuu31001, ty_Int) → new_esEs9(vuu3001, vuu31001)
new_esEs8(Left(vuu3000), Left(vuu31000), app(app(app(ty_@3, bdg), bdh), bea), bdb) → new_esEs12(vuu3000, vuu31000, bdg, bdh, bea)
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Bool) → new_esEs11(vuu3000, vuu31000)
new_esEs8(Right(vuu3000), Right(vuu31000), bee, ty_Bool) → new_esEs11(vuu3000, vuu31000)
new_primEqNat0(Succ(vuu30000), Succ(vuu310000)) → new_primEqNat0(vuu30000, vuu310000)
new_esEs9(vuu300, vuu3100) → new_primEqInt(vuu300, vuu3100)
new_esEs20(vuu3000, vuu31000, ty_Double) → new_esEs14(vuu3000, vuu31000)
new_esEs8(Left(vuu3000), Left(vuu31000), app(ty_Maybe, beb), bdb) → new_esEs5(vuu3000, vuu31000, beb)
new_esEs8(Right(vuu3000), Right(vuu31000), bee, app(ty_Ratio, bef)) → new_esEs7(vuu3000, vuu31000, bef)
new_esEs21(vuu3001, vuu31001, app(ty_Ratio, hb)) → new_esEs7(vuu3001, vuu31001, hb)
new_esEs23(vuu3000, vuu31000, app(app(ty_@2, bcg), bch)) → new_esEs15(vuu3000, vuu31000, bcg, bch)
new_primEqInt(Pos(Zero), Pos(Succ(vuu310000))) → False
new_primEqInt(Pos(Succ(vuu30000)), Pos(Zero)) → False
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs23(vuu3000, vuu31000, ty_Ordering) → new_esEs13(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, app(ty_[], bcb)) → new_esEs4(vuu3000, vuu31000, bcb)
new_esEs21(vuu3001, vuu31001, ty_Char) → new_esEs6(vuu3001, vuu31001)
The set Q consists of the following terms:
new_esEs10(@0, @0)
new_esEs8(Left(x0), Right(x1), x2, x3)
new_esEs8(Right(x0), Left(x1), x2, x3)
new_esEs22(x0, x1, ty_Integer)
new_esEs20(x0, x1, app(ty_[], x2))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs18(x0, x1, ty_Integer)
new_esEs8(Right(x0), Right(x1), x2, ty_Bool)
new_esEs8(Right(x0), Right(x1), x2, ty_Int)
new_esEs5(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs11(True, True)
new_esEs5(Just(x0), Just(x1), ty_Float)
new_esEs5(Just(x0), Just(x1), ty_Bool)
new_primEqNat0(Zero, Succ(x0))
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Integer)
new_esEs4([], :(x0, x1), x2)
new_esEs22(x0, x1, ty_Float)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs18(x0, x1, ty_Double)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_@0)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs5(Just(x0), Just(x1), ty_Integer)
new_esEs8(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs5(Just(x0), Just(x1), ty_Int)
new_esEs13(GT, GT)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs8(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs21(x0, x1, ty_Integer)
new_esEs18(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs20(x0, x1, ty_Char)
new_esEs4(:(x0, x1), :(x2, x3), x4)
new_esEs19(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_@0)
new_esEs18(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, ty_Bool)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs19(x0, x1, ty_Int)
new_esEs5(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs5(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs11(False, True)
new_esEs11(True, False)
new_esEs8(Right(x0), Right(x1), x2, app(ty_[], x3))
new_primMulNat0(Succ(x0), Zero)
new_esEs12(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_sr(Pos(x0), Pos(x1))
new_esEs6(Char(x0), Char(x1))
new_esEs8(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs19(x0, x1, app(ty_Ratio, x2))
new_esEs5(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, ty_Char)
new_esEs19(x0, x1, ty_Ordering)
new_esEs8(Right(x0), Right(x1), x2, ty_Double)
new_esEs25(x0, x1, ty_Integer)
new_esEs8(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(x0, x1, app(app(ty_@2, x2), x3))
new_esEs18(x0, x1, app(ty_Maybe, x2))
new_esEs19(x0, x1, app(ty_[], x2))
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs5(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Double)
new_esEs13(LT, GT)
new_esEs13(GT, LT)
new_esEs19(x0, x1, ty_Float)
new_esEs18(x0, x1, ty_Float)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_@0)
new_sr(Neg(x0), Neg(x1))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs15(@2(x0, x1), @2(x2, x3), x4, x5)
new_primEqNat0(Zero, Zero)
new_esEs8(Left(x0), Left(x1), ty_Int, x2)
new_esEs8(Left(x0), Left(x1), ty_@0, x2)
new_esEs14(Double(x0, x1), Double(x2, x3))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs21(x0, x1, ty_@0)
new_esEs13(EQ, GT)
new_esEs13(GT, EQ)
new_esEs7(:%(x0, x1), :%(x2, x3), x4)
new_esEs18(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(LT, LT)
new_esEs21(x0, x1, ty_Float)
new_esEs8(Left(x0), Left(x1), ty_Float, x2)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Integer)
new_primMulNat0(Zero, Zero)
new_esEs5(Just(x0), Just(x1), ty_Ordering)
new_esEs8(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs8(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs19(x0, x1, ty_Bool)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs8(Right(x0), Right(x1), x2, ty_Integer)
new_esEs21(x0, x1, ty_Ordering)
new_esEs5(Just(x0), Just(x1), ty_@0)
new_esEs23(x0, x1, ty_Bool)
new_esEs5(Nothing, Just(x0), x1)
new_esEs23(x0, x1, ty_Integer)
new_esEs8(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs22(x0, x1, ty_Int)
new_esEs13(EQ, LT)
new_esEs13(LT, EQ)
new_esEs8(Right(x0), Right(x1), x2, ty_Ordering)
new_primEqNat0(Succ(x0), Zero)
new_esEs19(x0, x1, ty_@0)
new_esEs13(EQ, EQ)
new_esEs23(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Double)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_Bool)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs8(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs5(Just(x0), Just(x1), app(ty_[], x2))
new_esEs5(Nothing, Nothing, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_asAs(True, x0)
new_primPlusNat1(Zero, Succ(x0))
new_esEs4(:(x0, x1), [], x2)
new_esEs19(x0, x1, ty_Double)
new_primPlusNat1(Succ(x0), Zero)
new_esEs23(x0, x1, ty_Double)
new_esEs8(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs8(Right(x0), Right(x1), x2, ty_@0)
new_esEs5(Just(x0), Just(x1), ty_Char)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs11(False, False)
new_esEs20(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Ordering)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs8(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs18(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Char)
new_esEs4([], [], x0)
new_esEs17(Float(x0, x1), Float(x2, x3))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs18(x0, x1, ty_@0)
new_esEs8(Left(x0), Left(x1), ty_Bool, x2)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Char)
new_esEs5(Just(x0), Nothing, x1)
new_esEs16(Integer(x0), Integer(x1))
new_primMulNat0(Zero, Succ(x0))
new_esEs20(x0, x1, ty_Double)
new_primPlusNat1(Zero, Zero)
new_esEs23(x0, x1, ty_Float)
new_esEs8(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_primPlusNat0(Succ(x0), x1)
new_esEs18(x0, x1, ty_Int)
new_asAs(False, x0)
new_esEs8(Left(x0), Left(x1), ty_Char, x2)
new_esEs18(x0, x1, app(ty_Ratio, x2))
new_esEs19(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs23(x0, x1, ty_Int)
new_esEs5(Just(x0), Just(x1), ty_Double)
new_primPlusNat0(Zero, x0)
new_esEs18(x0, x1, ty_Char)
new_esEs18(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Ordering)
new_esEs8(Right(x0), Right(x1), x2, ty_Char)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs8(Right(x0), Right(x1), x2, ty_Float)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs8(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs9(x0, x1)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_Int)
new_esEs8(Left(x0), Left(x1), ty_Integer, x2)
new_esEs20(x0, x1, ty_Int)
new_esEs18(x0, x1, ty_Ordering)
new_esEs19(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_Int)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs8(Left(x0), Left(x1), ty_Double, x2)
We have to consider all minimal (P,Q,R)-chains.
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [15] we can delete all non-usable rules [17] from R.
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_span2Zs1(vuu3110, vuu3111, True, ba) → new_span2Zs(vuu3111, ba)
new_span2Zs(:(vuu3110, vuu3111), ba) → new_span2Zs1(vuu3110, vuu3111, new_esEs4([], vuu3110, ba), ba)
new_span2Ys1(vuu3110, vuu3111, True, ba) → new_span2Zs(vuu3111, ba)
new_span2Ys1(vuu3110, vuu3111, True, ba) → new_span2Ys(vuu3111, ba)
new_span2Ys(:(vuu3110, vuu3111), ba) → new_span2Ys1(vuu3110, vuu3111, new_esEs4([], vuu3110, ba), ba)
new_span2Zs1(vuu3110, vuu3111, True, ba) → new_span2Ys(vuu3111, ba)
The TRS R consists of the following rules:
new_esEs4([], [], bbf) → True
new_esEs4([], :(vuu31000, vuu31001), bbf) → False
The set Q consists of the following terms:
new_esEs10(@0, @0)
new_esEs8(Left(x0), Right(x1), x2, x3)
new_esEs8(Right(x0), Left(x1), x2, x3)
new_esEs22(x0, x1, ty_Integer)
new_esEs20(x0, x1, app(ty_[], x2))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs18(x0, x1, ty_Integer)
new_esEs8(Right(x0), Right(x1), x2, ty_Bool)
new_esEs8(Right(x0), Right(x1), x2, ty_Int)
new_esEs5(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs11(True, True)
new_esEs5(Just(x0), Just(x1), ty_Float)
new_esEs5(Just(x0), Just(x1), ty_Bool)
new_primEqNat0(Zero, Succ(x0))
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Integer)
new_esEs4([], :(x0, x1), x2)
new_esEs22(x0, x1, ty_Float)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs18(x0, x1, ty_Double)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_@0)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs5(Just(x0), Just(x1), ty_Integer)
new_esEs8(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs5(Just(x0), Just(x1), ty_Int)
new_esEs13(GT, GT)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs8(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs21(x0, x1, ty_Integer)
new_esEs18(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs20(x0, x1, ty_Char)
new_esEs4(:(x0, x1), :(x2, x3), x4)
new_esEs19(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_@0)
new_esEs18(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, ty_Bool)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs19(x0, x1, ty_Int)
new_esEs5(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs5(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs11(False, True)
new_esEs11(True, False)
new_esEs8(Right(x0), Right(x1), x2, app(ty_[], x3))
new_primMulNat0(Succ(x0), Zero)
new_esEs12(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_sr(Pos(x0), Pos(x1))
new_esEs6(Char(x0), Char(x1))
new_esEs8(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs19(x0, x1, app(ty_Ratio, x2))
new_esEs5(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, ty_Char)
new_esEs19(x0, x1, ty_Ordering)
new_esEs8(Right(x0), Right(x1), x2, ty_Double)
new_esEs25(x0, x1, ty_Integer)
new_esEs8(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(x0, x1, app(app(ty_@2, x2), x3))
new_esEs18(x0, x1, app(ty_Maybe, x2))
new_esEs19(x0, x1, app(ty_[], x2))
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs5(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Double)
new_esEs13(LT, GT)
new_esEs13(GT, LT)
new_esEs19(x0, x1, ty_Float)
new_esEs18(x0, x1, ty_Float)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_@0)
new_sr(Neg(x0), Neg(x1))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs15(@2(x0, x1), @2(x2, x3), x4, x5)
new_primEqNat0(Zero, Zero)
new_esEs8(Left(x0), Left(x1), ty_Int, x2)
new_esEs8(Left(x0), Left(x1), ty_@0, x2)
new_esEs14(Double(x0, x1), Double(x2, x3))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs21(x0, x1, ty_@0)
new_esEs13(EQ, GT)
new_esEs13(GT, EQ)
new_esEs7(:%(x0, x1), :%(x2, x3), x4)
new_esEs18(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(LT, LT)
new_esEs21(x0, x1, ty_Float)
new_esEs8(Left(x0), Left(x1), ty_Float, x2)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Integer)
new_primMulNat0(Zero, Zero)
new_esEs5(Just(x0), Just(x1), ty_Ordering)
new_esEs8(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs8(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs19(x0, x1, ty_Bool)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs8(Right(x0), Right(x1), x2, ty_Integer)
new_esEs21(x0, x1, ty_Ordering)
new_esEs5(Just(x0), Just(x1), ty_@0)
new_esEs23(x0, x1, ty_Bool)
new_esEs5(Nothing, Just(x0), x1)
new_esEs23(x0, x1, ty_Integer)
new_esEs8(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs22(x0, x1, ty_Int)
new_esEs13(EQ, LT)
new_esEs13(LT, EQ)
new_esEs8(Right(x0), Right(x1), x2, ty_Ordering)
new_primEqNat0(Succ(x0), Zero)
new_esEs19(x0, x1, ty_@0)
new_esEs13(EQ, EQ)
new_esEs23(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Double)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_Bool)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs8(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs5(Just(x0), Just(x1), app(ty_[], x2))
new_esEs5(Nothing, Nothing, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_asAs(True, x0)
new_primPlusNat1(Zero, Succ(x0))
new_esEs4(:(x0, x1), [], x2)
new_esEs19(x0, x1, ty_Double)
new_primPlusNat1(Succ(x0), Zero)
new_esEs23(x0, x1, ty_Double)
new_esEs8(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs8(Right(x0), Right(x1), x2, ty_@0)
new_esEs5(Just(x0), Just(x1), ty_Char)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs11(False, False)
new_esEs20(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Ordering)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs8(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs18(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Char)
new_esEs4([], [], x0)
new_esEs17(Float(x0, x1), Float(x2, x3))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs18(x0, x1, ty_@0)
new_esEs8(Left(x0), Left(x1), ty_Bool, x2)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Char)
new_esEs5(Just(x0), Nothing, x1)
new_esEs16(Integer(x0), Integer(x1))
new_primMulNat0(Zero, Succ(x0))
new_esEs20(x0, x1, ty_Double)
new_primPlusNat1(Zero, Zero)
new_esEs23(x0, x1, ty_Float)
new_esEs8(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_primPlusNat0(Succ(x0), x1)
new_esEs18(x0, x1, ty_Int)
new_asAs(False, x0)
new_esEs8(Left(x0), Left(x1), ty_Char, x2)
new_esEs18(x0, x1, app(ty_Ratio, x2))
new_esEs19(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs23(x0, x1, ty_Int)
new_esEs5(Just(x0), Just(x1), ty_Double)
new_primPlusNat0(Zero, x0)
new_esEs18(x0, x1, ty_Char)
new_esEs18(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Ordering)
new_esEs8(Right(x0), Right(x1), x2, ty_Char)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs8(Right(x0), Right(x1), x2, ty_Float)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs8(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs9(x0, x1)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_Int)
new_esEs8(Left(x0), Left(x1), ty_Integer, x2)
new_esEs20(x0, x1, ty_Int)
new_esEs18(x0, x1, ty_Ordering)
new_esEs19(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_Int)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs8(Left(x0), Left(x1), ty_Double, x2)
We have to consider all minimal (P,Q,R)-chains.
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.
new_esEs10(@0, @0)
new_esEs8(Left(x0), Right(x1), x2, x3)
new_esEs8(Right(x0), Left(x1), x2, x3)
new_esEs22(x0, x1, ty_Integer)
new_esEs20(x0, x1, app(ty_[], x2))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs18(x0, x1, ty_Integer)
new_esEs8(Right(x0), Right(x1), x2, ty_Bool)
new_esEs8(Right(x0), Right(x1), x2, ty_Int)
new_esEs5(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs11(True, True)
new_esEs5(Just(x0), Just(x1), ty_Float)
new_esEs5(Just(x0), Just(x1), ty_Bool)
new_primEqNat0(Zero, Succ(x0))
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Float)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs18(x0, x1, ty_Double)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_@0)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs5(Just(x0), Just(x1), ty_Integer)
new_esEs8(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs5(Just(x0), Just(x1), ty_Int)
new_esEs13(GT, GT)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs8(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs21(x0, x1, ty_Integer)
new_esEs18(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs20(x0, x1, ty_Char)
new_esEs19(x0, x1, app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_@0)
new_esEs18(x0, x1, app(app(ty_@2, x2), x3))
new_esEs22(x0, x1, ty_Bool)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs19(x0, x1, ty_Int)
new_esEs5(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs5(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs11(False, True)
new_esEs11(True, False)
new_esEs8(Right(x0), Right(x1), x2, app(ty_[], x3))
new_primMulNat0(Succ(x0), Zero)
new_esEs12(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_sr(Pos(x0), Pos(x1))
new_esEs6(Char(x0), Char(x1))
new_esEs8(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs19(x0, x1, app(ty_Ratio, x2))
new_esEs5(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs21(x0, x1, ty_Char)
new_esEs19(x0, x1, ty_Ordering)
new_esEs8(Right(x0), Right(x1), x2, ty_Double)
new_esEs25(x0, x1, ty_Integer)
new_esEs8(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(x0, x1, app(app(ty_@2, x2), x3))
new_esEs18(x0, x1, app(ty_Maybe, x2))
new_esEs19(x0, x1, app(ty_[], x2))
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs5(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs21(x0, x1, ty_Double)
new_esEs13(LT, GT)
new_esEs13(GT, LT)
new_esEs19(x0, x1, ty_Float)
new_esEs18(x0, x1, ty_Float)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_@0)
new_sr(Neg(x0), Neg(x1))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs15(@2(x0, x1), @2(x2, x3), x4, x5)
new_primEqNat0(Zero, Zero)
new_esEs8(Left(x0), Left(x1), ty_Int, x2)
new_esEs8(Left(x0), Left(x1), ty_@0, x2)
new_esEs14(Double(x0, x1), Double(x2, x3))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs21(x0, x1, ty_@0)
new_esEs13(EQ, GT)
new_esEs13(GT, EQ)
new_esEs7(:%(x0, x1), :%(x2, x3), x4)
new_esEs18(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(LT, LT)
new_esEs21(x0, x1, ty_Float)
new_esEs8(Left(x0), Left(x1), ty_Float, x2)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Integer)
new_primMulNat0(Zero, Zero)
new_esEs5(Just(x0), Just(x1), ty_Ordering)
new_esEs8(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs8(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs19(x0, x1, ty_Bool)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs8(Right(x0), Right(x1), x2, ty_Integer)
new_esEs21(x0, x1, ty_Ordering)
new_esEs5(Just(x0), Just(x1), ty_@0)
new_esEs23(x0, x1, ty_Bool)
new_esEs5(Nothing, Just(x0), x1)
new_esEs23(x0, x1, ty_Integer)
new_esEs8(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs22(x0, x1, ty_Int)
new_esEs13(EQ, LT)
new_esEs13(LT, EQ)
new_esEs8(Right(x0), Right(x1), x2, ty_Ordering)
new_primEqNat0(Succ(x0), Zero)
new_esEs19(x0, x1, ty_@0)
new_esEs13(EQ, EQ)
new_esEs23(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Double)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_Bool)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs8(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs5(Just(x0), Just(x1), app(ty_[], x2))
new_esEs5(Nothing, Nothing, x0)
new_primMulNat0(Succ(x0), Succ(x1))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_asAs(True, x0)
new_primPlusNat1(Zero, Succ(x0))
new_esEs19(x0, x1, ty_Double)
new_primPlusNat1(Succ(x0), Zero)
new_esEs23(x0, x1, ty_Double)
new_esEs8(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs8(Right(x0), Right(x1), x2, ty_@0)
new_esEs5(Just(x0), Just(x1), ty_Char)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs11(False, False)
new_esEs20(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Ordering)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs8(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs18(x0, x1, app(app(ty_Either, x2), x3))
new_esEs22(x0, x1, ty_Char)
new_esEs17(Float(x0, x1), Float(x2, x3))
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs18(x0, x1, ty_@0)
new_esEs8(Left(x0), Left(x1), ty_Bool, x2)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Char)
new_esEs5(Just(x0), Nothing, x1)
new_esEs16(Integer(x0), Integer(x1))
new_primMulNat0(Zero, Succ(x0))
new_esEs20(x0, x1, ty_Double)
new_primPlusNat1(Zero, Zero)
new_esEs23(x0, x1, ty_Float)
new_esEs8(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_primPlusNat0(Succ(x0), x1)
new_esEs18(x0, x1, ty_Int)
new_asAs(False, x0)
new_esEs8(Left(x0), Left(x1), ty_Char, x2)
new_esEs18(x0, x1, app(ty_Ratio, x2))
new_esEs19(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs23(x0, x1, ty_Int)
new_esEs5(Just(x0), Just(x1), ty_Double)
new_primPlusNat0(Zero, x0)
new_esEs18(x0, x1, ty_Char)
new_esEs18(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, ty_Ordering)
new_esEs8(Right(x0), Right(x1), x2, ty_Char)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs8(Right(x0), Right(x1), x2, ty_Float)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs8(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs9(x0, x1)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_Int)
new_esEs8(Left(x0), Left(x1), ty_Integer, x2)
new_esEs20(x0, x1, ty_Int)
new_esEs18(x0, x1, ty_Ordering)
new_esEs19(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_Int)
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs8(Left(x0), Left(x1), ty_Double, x2)
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ UsableRulesProof
↳ QDP
↳ QReductionProof
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_span2Zs1(vuu3110, vuu3111, True, ba) → new_span2Zs(vuu3111, ba)
new_span2Ys1(vuu3110, vuu3111, True, ba) → new_span2Zs(vuu3111, ba)
new_span2Zs(:(vuu3110, vuu3111), ba) → new_span2Zs1(vuu3110, vuu3111, new_esEs4([], vuu3110, ba), ba)
new_span2Ys1(vuu3110, vuu3111, True, ba) → new_span2Ys(vuu3111, ba)
new_span2Ys(:(vuu3110, vuu3111), ba) → new_span2Ys1(vuu3110, vuu3111, new_esEs4([], vuu3110, ba), ba)
new_span2Zs1(vuu3110, vuu3111, True, ba) → new_span2Ys(vuu3111, ba)
The TRS R consists of the following rules:
new_esEs4([], [], bbf) → True
new_esEs4([], :(vuu31000, vuu31001), bbf) → False
The set Q consists of the following terms:
new_esEs4([], :(x0, x1), x2)
new_esEs4(:(x0, x1), :(x2, x3), x4)
new_esEs4(:(x0, x1), [], x2)
new_esEs4([], [], x0)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_span2Zs(:(vuu3110, vuu3111), ba) → new_span2Zs1(vuu3110, vuu3111, new_esEs4([], vuu3110, ba), ba)
The graph contains the following edges 1 > 1, 1 > 2, 2 >= 4
- new_span2Zs1(vuu3110, vuu3111, True, ba) → new_span2Zs(vuu3111, ba)
The graph contains the following edges 2 >= 1, 4 >= 2
- new_span2Zs1(vuu3110, vuu3111, True, ba) → new_span2Ys(vuu3111, ba)
The graph contains the following edges 2 >= 1, 4 >= 2
- new_span2Ys1(vuu3110, vuu3111, True, ba) → new_span2Zs(vuu3111, ba)
The graph contains the following edges 2 >= 1, 4 >= 2
- new_span2Ys(:(vuu3110, vuu3111), ba) → new_span2Ys1(vuu3110, vuu3111, new_esEs4([], vuu3110, ba), ba)
The graph contains the following edges 1 > 1, 1 > 2, 2 >= 4
- new_span2Ys1(vuu3110, vuu3111, True, ba) → new_span2Ys(vuu3111, ba)
The graph contains the following edges 2 >= 1, 4 >= 2
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPSizeChangeProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
new_span2Ys10(vuu11, vuu12, vuu150, vuu151, True, ba) → new_span2Zs0(vuu11, vuu12, vuu151, ba)
new_span2Zs10(vuu24, vuu25, vuu280, vuu281, True, bb) → new_span2Zs0(vuu24, vuu25, vuu281, bb)
new_span2Ys10(vuu11, vuu12, vuu150, vuu151, True, ba) → new_span2Ys0(vuu11, vuu12, vuu151, ba)
new_span2Ys0(vuu11, vuu12, :(vuu150, vuu151), ba) → new_span2Ys10(vuu11, vuu12, vuu150, vuu151, new_esEs4(:(vuu11, vuu12), vuu150, ba), ba)
new_span2Zs10(vuu24, vuu25, vuu280, vuu281, True, bb) → new_span2Ys0(vuu24, vuu25, vuu281, bb)
new_span2Zs0(vuu24, vuu25, :(vuu280, vuu281), bb) → new_span2Zs10(vuu24, vuu25, vuu280, vuu281, new_esEs4(:(vuu24, vuu25), vuu280, bb), bb)
The TRS R consists of the following rules:
new_esEs22(vuu3002, vuu31002, app(app(ty_@2, bbe), bbf)) → new_esEs15(vuu3002, vuu31002, bbe, bbf)
new_esEs8(Right(vuu3000), Right(vuu31000), bef, ty_Double) → new_esEs14(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, ty_Char) → new_esEs6(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, app(ty_Ratio, ga)) → new_esEs7(vuu3000, vuu31000, ga)
new_esEs8(Right(vuu3000), Right(vuu31000), bef, app(ty_[], bfb)) → new_esEs4(vuu3000, vuu31000, bfb)
new_primPlusNat1(Succ(vuu4900), Succ(vuu31000000)) → Succ(Succ(new_primPlusNat1(vuu4900, vuu31000000)))
new_esEs19(vuu3001, vuu31001, app(ty_Ratio, ec)) → new_esEs7(vuu3001, vuu31001, ec)
new_primEqInt(Neg(Succ(vuu30000)), Pos(vuu31000)) → False
new_primEqInt(Pos(Succ(vuu30000)), Neg(vuu31000)) → False
new_esEs18(vuu3000, vuu31000, ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs19(vuu3001, vuu31001, ty_Bool) → new_esEs11(vuu3001, vuu31001)
new_esEs8(Left(vuu3000), Left(vuu31000), app(ty_[], bdg), bdc) → new_esEs4(vuu3000, vuu31000, bdg)
new_primEqInt(Neg(Zero), Pos(Succ(vuu310000))) → False
new_primEqInt(Pos(Zero), Neg(Succ(vuu310000))) → False
new_esEs8(Right(vuu3000), Right(vuu31000), bef, ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, ty_Int) → new_esEs9(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, ty_Bool) → new_esEs11(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, app(app(ty_@2, ha), hb)) → new_esEs15(vuu3000, vuu31000, ha, hb)
new_esEs23(vuu3000, vuu31000, ty_Float) → new_esEs17(vuu3000, vuu31000)
new_esEs19(vuu3001, vuu31001, ty_Ordering) → new_esEs13(vuu3001, vuu31001)
new_primMulNat0(Zero, Zero) → Zero
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Double) → new_esEs14(vuu3000, vuu31000)
new_esEs15(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), cf, cg) → new_asAs(new_esEs18(vuu3000, vuu31000, cf), new_esEs19(vuu3001, vuu31001, cg))
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Int) → new_esEs9(vuu3000, vuu31000)
new_esEs21(vuu3001, vuu31001, app(app(ty_Either, hd), he)) → new_esEs8(vuu3001, vuu31001, hd, he)
new_esEs23(vuu3000, vuu31000, app(app(app(ty_@3, bcd), bce), bcf)) → new_esEs12(vuu3000, vuu31000, bcd, bce, bcf)
new_primPlusNat0(Zero, vuu3100000) → Succ(vuu3100000)
new_esEs21(vuu3001, vuu31001, app(app(ty_@2, bac), bad)) → new_esEs15(vuu3001, vuu31001, bac, bad)
new_esEs20(vuu3000, vuu31000, app(app(app(ty_@3, ge), gf), gg)) → new_esEs12(vuu3000, vuu31000, ge, gf, gg)
new_esEs13(EQ, EQ) → True
new_esEs12(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), ff, fg, fh) → new_asAs(new_esEs20(vuu3000, vuu31000, ff), new_asAs(new_esEs21(vuu3001, vuu31001, fg), new_esEs22(vuu3002, vuu31002, fh)))
new_sr(Neg(vuu30000), Pos(vuu310000)) → Neg(new_primMulNat0(vuu30000, vuu310000))
new_sr(Pos(vuu30000), Neg(vuu310000)) → Neg(new_primMulNat0(vuu30000, vuu310000))
new_esEs19(vuu3001, vuu31001, ty_Int) → new_esEs9(vuu3001, vuu31001)
new_esEs23(vuu3000, vuu31000, ty_@0) → new_esEs10(vuu3000, vuu31000)
new_esEs4(:(vuu3000, vuu3001), :(vuu31000, vuu31001), bbg) → new_asAs(new_esEs23(vuu3000, vuu31000, bbg), new_esEs4(vuu3001, vuu31001, bbg))
new_esEs22(vuu3002, vuu31002, ty_Bool) → new_esEs11(vuu3002, vuu31002)
new_esEs19(vuu3001, vuu31001, app(app(app(ty_@3, eg), eh), fa)) → new_esEs12(vuu3001, vuu31001, eg, eh, fa)
new_esEs21(vuu3001, vuu31001, ty_Integer) → new_esEs16(vuu3001, vuu31001)
new_esEs18(vuu3000, vuu31000, ty_Ordering) → new_esEs13(vuu3000, vuu31000)
new_esEs5(Just(vuu3000), Just(vuu31000), app(ty_Maybe, cc)) → new_esEs5(vuu3000, vuu31000, cc)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Float, bdc) → new_esEs17(vuu3000, vuu31000)
new_esEs24(vuu3000, vuu31000, ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs18(vuu3000, vuu31000, ty_Int) → new_esEs9(vuu3000, vuu31000)
new_esEs18(vuu3000, vuu31000, ty_Char) → new_esEs6(vuu3000, vuu31000)
new_esEs8(Right(vuu3000), Right(vuu31000), bef, ty_@0) → new_esEs10(vuu3000, vuu31000)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Double, bdc) → new_esEs14(vuu3000, vuu31000)
new_esEs13(GT, GT) → True
new_esEs8(Right(vuu3000), Right(vuu31000), bef, ty_Ordering) → new_esEs13(vuu3000, vuu31000)
new_primEqNat0(Zero, Succ(vuu310000)) → False
new_primEqNat0(Succ(vuu30000), Zero) → False
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Int, bdc) → new_esEs9(vuu3000, vuu31000)
new_esEs22(vuu3002, vuu31002, ty_Float) → new_esEs17(vuu3002, vuu31002)
new_esEs21(vuu3001, vuu31001, ty_Int) → new_esEs9(vuu3001, vuu31001)
new_esEs21(vuu3001, vuu31001, ty_@0) → new_esEs10(vuu3001, vuu31001)
new_esEs19(vuu3001, vuu31001, app(app(ty_@2, fc), fd)) → new_esEs15(vuu3001, vuu31001, fc, fd)
new_esEs22(vuu3002, vuu31002, ty_Char) → new_esEs6(vuu3002, vuu31002)
new_esEs17(Float(vuu3000, vuu3001), Float(vuu31000, vuu31001)) → new_esEs9(new_sr(vuu3000, vuu31000), new_sr(vuu3001, vuu31001))
new_esEs5(Just(vuu3000), Just(vuu31000), app(ty_Ratio, bd)) → new_esEs7(vuu3000, vuu31000, bd)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs22(vuu3002, vuu31002, ty_Double) → new_esEs14(vuu3002, vuu31002)
new_esEs13(EQ, LT) → False
new_esEs13(LT, EQ) → False
new_esEs20(vuu3000, vuu31000, ty_Ordering) → new_esEs13(vuu3000, vuu31000)
new_esEs14(Double(vuu3000, vuu3001), Double(vuu31000, vuu31001)) → new_esEs9(new_sr(vuu3000, vuu31000), new_sr(vuu3001, vuu31001))
new_esEs19(vuu3001, vuu31001, app(app(ty_Either, ed), ee)) → new_esEs8(vuu3001, vuu31001, ed, ee)
new_esEs22(vuu3002, vuu31002, ty_Ordering) → new_esEs13(vuu3002, vuu31002)
new_esEs22(vuu3002, vuu31002, ty_Int) → new_esEs9(vuu3002, vuu31002)
new_esEs18(vuu3000, vuu31000, app(app(app(ty_@3, de), df), dg)) → new_esEs12(vuu3000, vuu31000, de, df, dg)
new_esEs20(vuu3000, vuu31000, app(ty_[], gd)) → new_esEs4(vuu3000, vuu31000, gd)
new_esEs21(vuu3001, vuu31001, ty_Ordering) → new_esEs13(vuu3001, vuu31001)
new_esEs22(vuu3002, vuu31002, app(app(app(ty_@3, bba), bbb), bbc)) → new_esEs12(vuu3002, vuu31002, bba, bbb, bbc)
new_esEs19(vuu3001, vuu31001, app(ty_Maybe, fb)) → new_esEs5(vuu3001, vuu31001, fb)
new_esEs21(vuu3001, vuu31001, app(app(app(ty_@3, hg), hh), baa)) → new_esEs12(vuu3001, vuu31001, hg, hh, baa)
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Ordering) → new_esEs13(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, app(app(ty_Either, bca), bcb)) → new_esEs8(vuu3000, vuu31000, bca, bcb)
new_esEs22(vuu3002, vuu31002, ty_@0) → new_esEs10(vuu3002, vuu31002)
new_esEs24(vuu3000, vuu31000, ty_Int) → new_esEs9(vuu3000, vuu31000)
new_esEs25(vuu3001, vuu31001, ty_Integer) → new_esEs16(vuu3001, vuu31001)
new_esEs5(Just(vuu3000), Just(vuu31000), app(app(app(ty_@3, bh), ca), cb)) → new_esEs12(vuu3000, vuu31000, bh, ca, cb)
new_esEs18(vuu3000, vuu31000, app(app(ty_Either, db), dc)) → new_esEs8(vuu3000, vuu31000, db, dc)
new_esEs11(False, True) → False
new_esEs11(True, False) → False
new_esEs19(vuu3001, vuu31001, ty_Double) → new_esEs14(vuu3001, vuu31001)
new_esEs18(vuu3000, vuu31000, app(app(ty_@2, ea), eb)) → new_esEs15(vuu3000, vuu31000, ea, eb)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Char, bdc) → new_esEs6(vuu3000, vuu31000)
new_esEs8(Right(vuu3000), Right(vuu31000), bef, app(app(ty_@2, bfg), bfh)) → new_esEs15(vuu3000, vuu31000, bfg, bfh)
new_esEs23(vuu3000, vuu31000, ty_Double) → new_esEs14(vuu3000, vuu31000)
new_esEs16(Integer(vuu3000), Integer(vuu31000)) → new_primEqInt(vuu3000, vuu31000)
new_esEs8(Left(vuu3000), Left(vuu31000), app(app(ty_Either, bde), bdf), bdc) → new_esEs8(vuu3000, vuu31000, bde, bdf)
new_esEs8(Right(vuu3000), Right(vuu31000), bef, app(app(app(ty_@3, bfc), bfd), bfe)) → new_esEs12(vuu3000, vuu31000, bfc, bfd, bfe)
new_esEs21(vuu3001, vuu31001, ty_Bool) → new_esEs11(vuu3001, vuu31001)
new_esEs20(vuu3000, vuu31000, ty_Char) → new_esEs6(vuu3000, vuu31000)
new_esEs19(vuu3001, vuu31001, ty_Float) → new_esEs17(vuu3001, vuu31001)
new_esEs10(@0, @0) → True
new_esEs22(vuu3002, vuu31002, app(ty_Ratio, bae)) → new_esEs7(vuu3002, vuu31002, bae)
new_sr(Neg(vuu30000), Neg(vuu310000)) → Pos(new_primMulNat0(vuu30000, vuu310000))
new_esEs20(vuu3000, vuu31000, ty_Bool) → new_esEs11(vuu3000, vuu31000)
new_esEs21(vuu3001, vuu31001, app(ty_[], hf)) → new_esEs4(vuu3001, vuu31001, hf)
new_esEs20(vuu3000, vuu31000, app(ty_Maybe, gh)) → new_esEs5(vuu3000, vuu31000, gh)
new_esEs5(Just(vuu3000), Just(vuu31000), app(ty_[], bg)) → new_esEs4(vuu3000, vuu31000, bg)
new_asAs(False, vuu37) → False
new_sr(Pos(vuu30000), Pos(vuu310000)) → Pos(new_primMulNat0(vuu30000, vuu310000))
new_esEs7(:%(vuu3000, vuu3001), :%(vuu31000, vuu31001), bdb) → new_asAs(new_esEs24(vuu3000, vuu31000, bdb), new_esEs25(vuu3001, vuu31001, bdb))
new_primEqNat0(Zero, Zero) → True
new_primMulNat0(Zero, Succ(vuu3100000)) → Zero
new_primMulNat0(Succ(vuu300000), Zero) → Zero
new_esEs13(GT, EQ) → False
new_esEs13(EQ, GT) → False
new_esEs13(GT, LT) → False
new_esEs13(LT, GT) → False
new_esEs23(vuu3000, vuu31000, ty_Int) → new_esEs9(vuu3000, vuu31000)
new_esEs18(vuu3000, vuu31000, app(ty_Maybe, dh)) → new_esEs5(vuu3000, vuu31000, dh)
new_esEs18(vuu3000, vuu31000, app(ty_[], dd)) → new_esEs4(vuu3000, vuu31000, dd)
new_esEs8(Right(vuu3000), Right(vuu31000), bef, app(ty_Maybe, bff)) → new_esEs5(vuu3000, vuu31000, bff)
new_esEs11(True, True) → True
new_esEs23(vuu3000, vuu31000, app(ty_Maybe, bcg)) → new_esEs5(vuu3000, vuu31000, bcg)
new_esEs8(Left(vuu3000), Left(vuu31000), app(ty_Ratio, bdd), bdc) → new_esEs7(vuu3000, vuu31000, bdd)
new_esEs5(Just(vuu3000), Just(vuu31000), app(app(ty_@2, cd), ce)) → new_esEs15(vuu3000, vuu31000, cd, ce)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Ordering, bdc) → new_esEs13(vuu3000, vuu31000)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Bool, bdc) → new_esEs11(vuu3000, vuu31000)
new_primPlusNat0(Succ(vuu490), vuu3100000) → Succ(Succ(new_primPlusNat1(vuu490, vuu3100000)))
new_esEs8(Left(vuu3000), Left(vuu31000), app(app(ty_@2, bed), bee), bdc) → new_esEs15(vuu3000, vuu31000, bed, bee)
new_esEs5(Just(vuu3000), Just(vuu31000), app(app(ty_Either, be), bf)) → new_esEs8(vuu3000, vuu31000, be, bf)
new_esEs5(Just(vuu3000), Nothing, bc) → False
new_esEs5(Nothing, Just(vuu31000), bc) → False
new_esEs19(vuu3001, vuu31001, ty_Integer) → new_esEs16(vuu3001, vuu31001)
new_esEs19(vuu3001, vuu31001, ty_Char) → new_esEs6(vuu3001, vuu31001)
new_primEqInt(Neg(Succ(vuu30000)), Neg(Succ(vuu310000))) → new_primEqNat0(vuu30000, vuu310000)
new_esEs4([], [], bbg) → True
new_esEs20(vuu3000, vuu31000, ty_Float) → new_esEs17(vuu3000, vuu31000)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_@0, bdc) → new_esEs10(vuu3000, vuu31000)
new_esEs18(vuu3000, vuu31000, ty_@0) → new_esEs10(vuu3000, vuu31000)
new_primPlusNat1(Succ(vuu4900), Zero) → Succ(vuu4900)
new_primPlusNat1(Zero, Succ(vuu31000000)) → Succ(vuu31000000)
new_esEs23(vuu3000, vuu31000, app(ty_Ratio, bbh)) → new_esEs7(vuu3000, vuu31000, bbh)
new_esEs8(Right(vuu3000), Right(vuu31000), bef, app(app(ty_Either, beh), bfa)) → new_esEs8(vuu3000, vuu31000, beh, bfa)
new_esEs8(Right(vuu3000), Left(vuu31000), bef, bdc) → False
new_esEs8(Left(vuu3000), Right(vuu31000), bef, bdc) → False
new_esEs18(vuu3000, vuu31000, app(ty_Ratio, da)) → new_esEs7(vuu3000, vuu31000, da)
new_esEs6(Char(vuu3000), Char(vuu31000)) → new_primEqNat0(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, app(app(ty_Either, gb), gc)) → new_esEs8(vuu3000, vuu31000, gb, gc)
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Float) → new_esEs17(vuu3000, vuu31000)
new_esEs21(vuu3001, vuu31001, ty_Double) → new_esEs14(vuu3001, vuu31001)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs18(vuu3000, vuu31000, ty_Float) → new_esEs17(vuu3000, vuu31000)
new_esEs5(Nothing, Nothing, bc) → True
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs18(vuu3000, vuu31000, ty_Bool) → new_esEs11(vuu3000, vuu31000)
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Char) → new_esEs6(vuu3000, vuu31000)
new_esEs22(vuu3002, vuu31002, ty_Integer) → new_esEs16(vuu3002, vuu31002)
new_primEqInt(Neg(Zero), Neg(Succ(vuu310000))) → False
new_primEqInt(Neg(Succ(vuu30000)), Neg(Zero)) → False
new_esEs23(vuu3000, vuu31000, ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs4([], :(vuu31000, vuu31001), bbg) → False
new_esEs4(:(vuu3000, vuu3001), [], bbg) → False
new_esEs20(vuu3000, vuu31000, ty_@0) → new_esEs10(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs22(vuu3002, vuu31002, app(ty_Maybe, bbd)) → new_esEs5(vuu3002, vuu31002, bbd)
new_esEs21(vuu3001, vuu31001, app(ty_Maybe, bab)) → new_esEs5(vuu3001, vuu31001, bab)
new_primPlusNat1(Zero, Zero) → Zero
new_esEs21(vuu3001, vuu31001, ty_Float) → new_esEs17(vuu3001, vuu31001)
new_asAs(True, vuu37) → vuu37
new_esEs5(Just(vuu3000), Just(vuu31000), ty_@0) → new_esEs10(vuu3000, vuu31000)
new_primMulNat0(Succ(vuu300000), Succ(vuu3100000)) → new_primPlusNat0(new_primMulNat0(vuu300000, Succ(vuu3100000)), vuu3100000)
new_esEs19(vuu3001, vuu31001, app(ty_[], ef)) → new_esEs4(vuu3001, vuu31001, ef)
new_esEs8(Right(vuu3000), Right(vuu31000), bef, ty_Int) → new_esEs9(vuu3000, vuu31000)
new_esEs13(LT, LT) → True
new_esEs18(vuu3000, vuu31000, ty_Double) → new_esEs14(vuu3000, vuu31000)
new_esEs22(vuu3002, vuu31002, app(ty_[], bah)) → new_esEs4(vuu3002, vuu31002, bah)
new_esEs11(False, False) → True
new_primEqInt(Pos(Succ(vuu30000)), Pos(Succ(vuu310000))) → new_primEqNat0(vuu30000, vuu310000)
new_esEs8(Right(vuu3000), Right(vuu31000), bef, ty_Char) → new_esEs6(vuu3000, vuu31000)
new_esEs8(Right(vuu3000), Right(vuu31000), bef, ty_Float) → new_esEs17(vuu3000, vuu31000)
new_esEs19(vuu3001, vuu31001, ty_@0) → new_esEs10(vuu3001, vuu31001)
new_esEs22(vuu3002, vuu31002, app(app(ty_Either, baf), bag)) → new_esEs8(vuu3002, vuu31002, baf, bag)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Integer, bdc) → new_esEs16(vuu3000, vuu31000)
new_esEs25(vuu3001, vuu31001, ty_Int) → new_esEs9(vuu3001, vuu31001)
new_esEs8(Left(vuu3000), Left(vuu31000), app(app(app(ty_@3, bdh), bea), beb), bdc) → new_esEs12(vuu3000, vuu31000, bdh, bea, beb)
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Bool) → new_esEs11(vuu3000, vuu31000)
new_esEs8(Right(vuu3000), Right(vuu31000), bef, ty_Bool) → new_esEs11(vuu3000, vuu31000)
new_primEqNat0(Succ(vuu30000), Succ(vuu310000)) → new_primEqNat0(vuu30000, vuu310000)
new_esEs9(vuu300, vuu3100) → new_primEqInt(vuu300, vuu3100)
new_esEs20(vuu3000, vuu31000, ty_Double) → new_esEs14(vuu3000, vuu31000)
new_esEs8(Left(vuu3000), Left(vuu31000), app(ty_Maybe, bec), bdc) → new_esEs5(vuu3000, vuu31000, bec)
new_esEs8(Right(vuu3000), Right(vuu31000), bef, app(ty_Ratio, beg)) → new_esEs7(vuu3000, vuu31000, beg)
new_esEs21(vuu3001, vuu31001, app(ty_Ratio, hc)) → new_esEs7(vuu3001, vuu31001, hc)
new_esEs23(vuu3000, vuu31000, app(app(ty_@2, bch), bda)) → new_esEs15(vuu3000, vuu31000, bch, bda)
new_primEqInt(Pos(Zero), Pos(Succ(vuu310000))) → False
new_primEqInt(Pos(Succ(vuu30000)), Pos(Zero)) → False
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs23(vuu3000, vuu31000, ty_Ordering) → new_esEs13(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, app(ty_[], bcc)) → new_esEs4(vuu3000, vuu31000, bcc)
new_esEs21(vuu3001, vuu31001, ty_Char) → new_esEs6(vuu3001, vuu31001)
The set Q consists of the following terms:
new_esEs10(@0, @0)
new_esEs22(x0, x1, ty_Integer)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs18(x0, x1, ty_Integer)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs8(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs11(True, True)
new_esEs5(Just(x0), Just(x1), ty_Float)
new_esEs5(Just(x0), Just(x1), ty_Bool)
new_primEqNat0(Zero, Succ(x0))
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs20(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Float)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs18(x0, x1, ty_Double)
new_esEs23(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Float)
new_esEs22(x0, x1, ty_@0)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs5(Just(x0), Just(x1), ty_Integer)
new_esEs8(Right(x0), Right(x1), x2, ty_Int)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs5(Just(x0), Just(x1), ty_Int)
new_esEs8(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(GT, GT)
new_esEs7(:%(x0, x1), :%(x2, x3), x4)
new_esEs8(Left(x0), Left(x1), ty_Bool, x2)
new_esEs22(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs21(x0, x1, ty_Integer)
new_esEs18(x0, x1, app(app(ty_@2, x2), x3))
new_esEs18(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs20(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Bool)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs15(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs21(x0, x1, ty_Int)
new_esEs8(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs19(x0, x1, ty_Int)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs11(False, True)
new_esEs11(True, False)
new_esEs4([], [], x0)
new_primMulNat0(Succ(x0), Zero)
new_esEs5(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_sr(Pos(x0), Pos(x1))
new_esEs6(Char(x0), Char(x1))
new_esEs19(x0, x1, app(ty_[], x2))
new_esEs8(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs8(Right(x0), Right(x1), x2, ty_Double)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_Char)
new_esEs19(x0, x1, ty_Ordering)
new_esEs8(Right(x0), Right(x1), x2, ty_Char)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs25(x0, x1, ty_Integer)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs18(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Double)
new_esEs19(x0, x1, app(ty_Maybe, x2))
new_esEs13(LT, GT)
new_esEs13(GT, LT)
new_esEs8(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs19(x0, x1, ty_Float)
new_esEs18(x0, x1, ty_Float)
new_esEs23(x0, x1, ty_@0)
new_sr(Neg(x0), Neg(x1))
new_esEs5(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs8(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_primEqNat0(Zero, Zero)
new_esEs8(Right(x0), Right(x1), x2, ty_Float)
new_esEs8(Left(x0), Left(x1), ty_Float, x2)
new_esEs5(Just(x0), Just(x1), app(ty_[], x2))
new_esEs14(Double(x0, x1), Double(x2, x3))
new_esEs19(x0, x1, app(app(ty_@2, x2), x3))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs21(x0, x1, ty_@0)
new_esEs8(Left(x0), Left(x1), ty_Int, x2)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs8(Right(x0), Right(x1), x2, ty_@0)
new_esEs13(EQ, GT)
new_esEs13(GT, EQ)
new_esEs13(LT, LT)
new_esEs21(x0, x1, ty_Float)
new_esEs8(Left(x0), Left(x1), ty_Double, x2)
new_esEs8(Left(x0), Left(x1), ty_Char, x2)
new_esEs24(x0, x1, ty_Integer)
new_primMulNat0(Zero, Zero)
new_esEs5(Just(x0), Just(x1), ty_Ordering)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs18(x0, x1, app(ty_Maybe, x2))
new_esEs19(x0, x1, ty_Bool)
new_esEs4(:(x0, x1), [], x2)
new_esEs8(Left(x0), Left(x1), ty_Integer, x2)
new_esEs21(x0, x1, ty_Ordering)
new_esEs5(Just(x0), Just(x1), ty_@0)
new_esEs23(x0, x1, ty_Bool)
new_esEs23(x0, x1, ty_Integer)
new_esEs4(:(x0, x1), :(x2, x3), x4)
new_esEs8(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs22(x0, x1, ty_Int)
new_esEs13(EQ, LT)
new_esEs13(LT, EQ)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs5(Nothing, Nothing, x0)
new_primEqNat0(Succ(x0), Zero)
new_esEs18(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs19(x0, x1, ty_@0)
new_esEs13(EQ, EQ)
new_esEs18(x0, x1, app(ty_Ratio, x2))
new_esEs23(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_Bool)
new_primMulNat0(Succ(x0), Succ(x1))
new_esEs5(Nothing, Just(x0), x1)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs20(x0, x1, app(ty_[], x2))
new_asAs(True, x0)
new_primPlusNat1(Zero, Succ(x0))
new_esEs19(x0, x1, app(ty_Ratio, x2))
new_esEs19(x0, x1, ty_Double)
new_primPlusNat1(Succ(x0), Zero)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Double)
new_esEs5(Just(x0), Just(x1), ty_Char)
new_esEs8(Left(x0), Right(x1), x2, x3)
new_esEs8(Right(x0), Left(x1), x2, x3)
new_esEs11(False, False)
new_esEs5(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs20(x0, x1, ty_Bool)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Ordering)
new_esEs8(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs22(x0, x1, ty_Char)
new_esEs17(Float(x0, x1), Float(x2, x3))
new_esEs18(x0, x1, ty_@0)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Char)
new_esEs5(Just(x0), Just(x1), app(ty_Ratio, x2))
new_esEs16(Integer(x0), Integer(x1))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs8(Left(x0), Left(x1), ty_@0, x2)
new_primMulNat0(Zero, Succ(x0))
new_esEs20(x0, x1, ty_Double)
new_primPlusNat1(Zero, Zero)
new_esEs23(x0, x1, ty_Float)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_primPlusNat0(Succ(x0), x1)
new_esEs8(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs18(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs4([], :(x0, x1), x2)
new_esEs5(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs18(x0, x1, ty_Int)
new_asAs(False, x0)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs23(x0, x1, ty_Int)
new_esEs8(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs8(Right(x0), Right(x1), x2, ty_Integer)
new_esEs5(Just(x0), Just(x1), ty_Double)
new_esEs8(Left(x0), Left(x1), app(ty_[], x2), x3)
new_primPlusNat0(Zero, x0)
new_esEs18(x0, x1, ty_Char)
new_esEs20(x0, x1, ty_Ordering)
new_esEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(Just(x0), Nothing, x1)
new_esEs8(Right(x0), Right(x1), x2, ty_Bool)
new_esEs8(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs9(x0, x1)
new_esEs25(x0, x1, ty_Int)
new_esEs20(x0, x1, ty_Int)
new_esEs18(x0, x1, ty_Ordering)
new_esEs19(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs8(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs12(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem. From the DPs we obtained the following set of size-change graphs:
- new_span2Zs0(vuu24, vuu25, :(vuu280, vuu281), bb) → new_span2Zs10(vuu24, vuu25, vuu280, vuu281, new_esEs4(:(vuu24, vuu25), vuu280, bb), bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 3 > 4, 4 >= 6
- new_span2Ys0(vuu11, vuu12, :(vuu150, vuu151), ba) → new_span2Ys10(vuu11, vuu12, vuu150, vuu151, new_esEs4(:(vuu11, vuu12), vuu150, ba), ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3, 3 > 4, 4 >= 6
- new_span2Ys10(vuu11, vuu12, vuu150, vuu151, True, ba) → new_span2Ys0(vuu11, vuu12, vuu151, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 6 >= 4
- new_span2Ys10(vuu11, vuu12, vuu150, vuu151, True, ba) → new_span2Zs0(vuu11, vuu12, vuu151, ba)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 6 >= 4
- new_span2Zs10(vuu24, vuu25, vuu280, vuu281, True, bb) → new_span2Ys0(vuu24, vuu25, vuu281, bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 6 >= 4
- new_span2Zs10(vuu24, vuu25, vuu280, vuu281, True, bb) → new_span2Zs0(vuu24, vuu25, vuu281, bb)
The graph contains the following edges 1 >= 1, 2 >= 2, 4 >= 3, 6 >= 4
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
Q DP problem:
The TRS P consists of the following rules:
new_groupBy(:(vuu30, vuu31), ba) → new_groupBy(new_groupByZs0(vuu30, vuu31, ba), ba)
The TRS R consists of the following rules:
new_esEs22(vuu3002, vuu31002, app(app(ty_@2, bdd), bde)) → new_esEs15(vuu3002, vuu31002, bdd, bde)
new_esEs23(vuu3000, vuu31000, ty_Char) → new_esEs6(vuu3000, vuu31000)
new_esEs8(Right(vuu3000), Right(vuu31000), hc, ty_Double) → new_esEs14(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, app(ty_Ratio, hh)) → new_esEs7(vuu3000, vuu31000, hh)
new_esEs8(Right(vuu3000), Right(vuu31000), hc, app(ty_[], bfc)) → new_esEs4(vuu3000, vuu31000, bfc)
new_esEs26(vuu300, vuu3100, app(app(app(ty_@3, he), hf), hg)) → new_esEs12(vuu300, vuu3100, he, hf, hg)
new_primPlusNat1(Succ(vuu4900), Succ(vuu31000000)) → Succ(Succ(new_primPlusNat1(vuu4900, vuu31000000)))
new_esEs19(vuu3001, vuu31001, app(ty_Ratio, fh)) → new_esEs7(vuu3001, vuu31001, fh)
new_primEqInt(Pos(Succ(vuu30000)), Neg(vuu31000)) → False
new_primEqInt(Neg(Succ(vuu30000)), Pos(vuu31000)) → False
new_esEs18(vuu3000, vuu31000, ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs19(vuu3001, vuu31001, ty_Bool) → new_esEs11(vuu3001, vuu31001)
new_esEs8(Left(vuu3000), Left(vuu31000), app(ty_[], bea), hd) → new_esEs4(vuu3000, vuu31000, bea)
new_esEs26(vuu300, vuu3100, ty_Double) → new_esEs14(vuu300, vuu3100)
new_esEs26(vuu300, vuu3100, ty_Int) → new_esEs9(vuu300, vuu3100)
new_primEqInt(Pos(Zero), Neg(Succ(vuu310000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(vuu310000))) → False
new_span2Zs12(vuu3110, vuu3111, True, ba) → new_span2Zs13(vuu3110, vuu3111, new_span2Ys3(vuu3111, ba), new_span2Zs3(vuu3111, ba), ba)
new_esEs8(Right(vuu3000), Right(vuu31000), hc, ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, ty_Int) → new_esEs9(vuu3000, vuu31000)
new_span2Zs12(vuu3110, vuu3111, False, ba) → :(vuu3110, vuu3111)
new_esEs23(vuu3000, vuu31000, ty_Bool) → new_esEs11(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, app(app(ty_@2, bah), bba)) → new_esEs15(vuu3000, vuu31000, bah, bba)
new_esEs23(vuu3000, vuu31000, ty_Float) → new_esEs17(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, ty_Float) → new_esEs17(vuu300, vuu3100)
new_esEs26(vuu300, vuu3100, app(app(ty_@2, ec), ed)) → new_esEs15(vuu300, vuu3100, ec, ed)
new_esEs19(vuu3001, vuu31001, ty_Ordering) → new_esEs13(vuu3001, vuu31001)
new_primMulNat0(Zero, Zero) → Zero
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Double) → new_esEs14(vuu3000, vuu31000)
new_esEs15(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), ec, ed) → new_asAs(new_esEs18(vuu3000, vuu31000, ec), new_esEs19(vuu3001, vuu31001, ed))
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Int) → new_esEs9(vuu3000, vuu31000)
new_span2Ys14(vuu3110, vuu3111, vuu43, vuu42, ba) → :(vuu3110, vuu43)
new_esEs21(vuu3001, vuu31001, app(app(ty_Either, bbc), bbd)) → new_esEs8(vuu3001, vuu31001, bbc, bbd)
new_esEs26(vuu300, vuu3100, app(ty_Ratio, hb)) → new_esEs7(vuu300, vuu3100, hb)
new_esEs23(vuu3000, vuu31000, app(app(app(ty_@3, bh), ca), cb)) → new_esEs12(vuu3000, vuu31000, bh, ca, cb)
new_primPlusNat0(Zero, vuu3100000) → Succ(vuu3100000)
new_esEs21(vuu3001, vuu31001, app(app(ty_@2, bcb), bcc)) → new_esEs15(vuu3001, vuu31001, bcb, bcc)
new_esEs20(vuu3000, vuu31000, app(app(app(ty_@3, bad), bae), baf)) → new_esEs12(vuu3000, vuu31000, bad, bae, baf)
new_esEs12(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), he, hf, hg) → new_asAs(new_esEs20(vuu3000, vuu31000, he), new_asAs(new_esEs21(vuu3001, vuu31001, hf), new_esEs22(vuu3002, vuu31002, hg)))
new_esEs13(EQ, EQ) → True
new_sr(Neg(vuu30000), Pos(vuu310000)) → Neg(new_primMulNat0(vuu30000, vuu310000))
new_sr(Pos(vuu30000), Neg(vuu310000)) → Neg(new_primMulNat0(vuu30000, vuu310000))
new_esEs19(vuu3001, vuu31001, ty_Int) → new_esEs9(vuu3001, vuu31001)
new_span2Zs14(vuu24, vuu25, vuu280, vuu281, vuu51, vuu50, bb) → vuu50
new_esEs23(vuu3000, vuu31000, ty_@0) → new_esEs10(vuu3000, vuu31000)
new_esEs4(:(vuu3000, vuu3001), :(vuu31000, vuu31001), bc) → new_asAs(new_esEs23(vuu3000, vuu31000, bc), new_esEs4(vuu3001, vuu31001, bc))
new_span2Ys13(vuu3110, vuu3111, True, ba) → new_span2Ys14(vuu3110, vuu3111, new_span2Ys3(vuu3111, ba), new_span2Zs3(vuu3111, ba), ba)
new_esEs22(vuu3002, vuu31002, ty_Bool) → new_esEs11(vuu3002, vuu31002)
new_groupByZs0(:(vuu300, vuu301), :([], vuu311), ba) → :([], vuu311)
new_esEs19(vuu3001, vuu31001, app(app(app(ty_@3, gd), ge), gf)) → new_esEs12(vuu3001, vuu31001, gd, ge, gf)
new_esEs21(vuu3001, vuu31001, ty_Integer) → new_esEs16(vuu3001, vuu31001)
new_esEs18(vuu3000, vuu31000, ty_Ordering) → new_esEs13(vuu3000, vuu31000)
new_esEs5(Just(vuu3000), Just(vuu31000), app(ty_Maybe, dh)) → new_esEs5(vuu3000, vuu31000, dh)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Float, hd) → new_esEs17(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, ty_@0) → new_esEs10(vuu300, vuu3100)
new_esEs24(vuu3000, vuu31000, ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs18(vuu3000, vuu31000, ty_Int) → new_esEs9(vuu3000, vuu31000)
new_esEs18(vuu3000, vuu31000, ty_Char) → new_esEs6(vuu3000, vuu31000)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Double, hd) → new_esEs14(vuu3000, vuu31000)
new_esEs8(Right(vuu3000), Right(vuu31000), hc, ty_@0) → new_esEs10(vuu3000, vuu31000)
new_esEs13(GT, GT) → True
new_esEs8(Right(vuu3000), Right(vuu31000), hc, ty_Ordering) → new_esEs13(vuu3000, vuu31000)
new_primEqNat0(Zero, Succ(vuu310000)) → False
new_primEqNat0(Succ(vuu30000), Zero) → False
new_esEs22(vuu3002, vuu31002, ty_Float) → new_esEs17(vuu3002, vuu31002)
new_esEs21(vuu3001, vuu31001, ty_@0) → new_esEs10(vuu3001, vuu31001)
new_esEs21(vuu3001, vuu31001, ty_Int) → new_esEs9(vuu3001, vuu31001)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Int, hd) → new_esEs9(vuu3000, vuu31000)
new_esEs19(vuu3001, vuu31001, app(app(ty_@2, gh), ha)) → new_esEs15(vuu3001, vuu31001, gh, ha)
new_esEs22(vuu3002, vuu31002, ty_Char) → new_esEs6(vuu3002, vuu31002)
new_esEs17(Float(vuu3000, vuu3001), Float(vuu31000, vuu31001)) → new_esEs9(new_sr(vuu3000, vuu31000), new_sr(vuu3001, vuu31001))
new_esEs5(Just(vuu3000), Just(vuu31000), app(ty_Ratio, da)) → new_esEs7(vuu3000, vuu31000, da)
new_esEs22(vuu3002, vuu31002, ty_Double) → new_esEs14(vuu3002, vuu31002)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_span2Ys13(vuu3110, vuu3111, False, ba) → []
new_esEs13(LT, EQ) → False
new_esEs13(EQ, LT) → False
new_esEs20(vuu3000, vuu31000, ty_Ordering) → new_esEs13(vuu3000, vuu31000)
new_esEs14(Double(vuu3000, vuu3001), Double(vuu31000, vuu31001)) → new_esEs9(new_sr(vuu3000, vuu31000), new_sr(vuu3001, vuu31001))
new_esEs19(vuu3001, vuu31001, app(app(ty_Either, ga), gb)) → new_esEs8(vuu3001, vuu31001, ga, gb)
new_span2Ys12(vuu11, vuu12, vuu150, vuu151, vuu47, vuu46, cf) → :(vuu150, vuu47)
new_esEs22(vuu3002, vuu31002, ty_Ordering) → new_esEs13(vuu3002, vuu31002)
new_esEs22(vuu3002, vuu31002, ty_Int) → new_esEs9(vuu3002, vuu31002)
new_esEs18(vuu3000, vuu31000, app(app(app(ty_@3, fa), fb), fc)) → new_esEs12(vuu3000, vuu31000, fa, fb, fc)
new_esEs20(vuu3000, vuu31000, app(ty_[], bac)) → new_esEs4(vuu3000, vuu31000, bac)
new_esEs21(vuu3001, vuu31001, ty_Ordering) → new_esEs13(vuu3001, vuu31001)
new_esEs22(vuu3002, vuu31002, app(app(app(ty_@3, bch), bda), bdb)) → new_esEs12(vuu3002, vuu31002, bch, bda, bdb)
new_esEs21(vuu3001, vuu31001, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs12(vuu3001, vuu31001, bbf, bbg, bbh)
new_esEs19(vuu3001, vuu31001, app(ty_Maybe, gg)) → new_esEs5(vuu3001, vuu31001, gg)
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Ordering) → new_esEs13(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, app(app(ty_Either, be), bf)) → new_esEs8(vuu3000, vuu31000, be, bf)
new_esEs26(vuu300, vuu3100, app(ty_Maybe, cg)) → new_esEs5(vuu300, vuu3100, cg)
new_esEs22(vuu3002, vuu31002, ty_@0) → new_esEs10(vuu3002, vuu31002)
new_esEs26(vuu300, vuu3100, app(app(ty_Either, hc), hd)) → new_esEs8(vuu300, vuu3100, hc, hd)
new_esEs24(vuu3000, vuu31000, ty_Int) → new_esEs9(vuu3000, vuu31000)
new_esEs25(vuu3001, vuu31001, ty_Integer) → new_esEs16(vuu3001, vuu31001)
new_esEs5(Just(vuu3000), Just(vuu31000), app(app(app(ty_@3, de), df), dg)) → new_esEs12(vuu3000, vuu31000, de, df, dg)
new_groupByZs00(vuu24, vuu25, vuu26, vuu27, vuu28, True, True, bb) → new_groupByZs02(vuu24, vuu25, vuu26, vuu27, vuu28, new_span2Ys2(vuu24, vuu25, vuu28, bb), bb)
new_esEs18(vuu3000, vuu31000, app(app(ty_Either, ef), eg)) → new_esEs8(vuu3000, vuu31000, ef, eg)
new_groupByZs01(vuu24, vuu25, vuu26, vuu27, vuu28, bb) → :(:(vuu26, vuu27), vuu28)
new_esEs11(False, True) → False
new_esEs11(True, False) → False
new_esEs19(vuu3001, vuu31001, ty_Double) → new_esEs14(vuu3001, vuu31001)
new_esEs18(vuu3000, vuu31000, app(app(ty_@2, ff), fg)) → new_esEs15(vuu3000, vuu31000, ff, fg)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Char, hd) → new_esEs6(vuu3000, vuu31000)
new_esEs8(Right(vuu3000), Right(vuu31000), hc, app(app(ty_@2, bfh), bga)) → new_esEs15(vuu3000, vuu31000, bfh, bga)
new_esEs23(vuu3000, vuu31000, ty_Double) → new_esEs14(vuu3000, vuu31000)
new_esEs16(Integer(vuu3000), Integer(vuu31000)) → new_primEqInt(vuu3000, vuu31000)
new_esEs8(Left(vuu3000), Left(vuu31000), app(app(ty_Either, bdg), bdh), hd) → new_esEs8(vuu3000, vuu31000, bdg, bdh)
new_groupByZs0(:(vuu300, vuu301), :(:(vuu3100, vuu3101), vuu311), ba) → new_groupByZs00(vuu300, vuu301, vuu3100, vuu3101, vuu311, new_esEs26(vuu300, vuu3100, ba), new_esEs4(vuu301, vuu3101, ba), ba)
new_esEs8(Right(vuu3000), Right(vuu31000), hc, app(app(app(ty_@3, bfd), bfe), bff)) → new_esEs12(vuu3000, vuu31000, bfd, bfe, bff)
new_esEs21(vuu3001, vuu31001, ty_Bool) → new_esEs11(vuu3001, vuu31001)
new_esEs26(vuu300, vuu3100, ty_Bool) → new_esEs11(vuu300, vuu3100)
new_groupByZs0(vuu30, [], ba) → []
new_esEs20(vuu3000, vuu31000, ty_Char) → new_esEs6(vuu3000, vuu31000)
new_esEs19(vuu3001, vuu31001, ty_Float) → new_esEs17(vuu3001, vuu31001)
new_esEs10(@0, @0) → True
new_groupByZs00(vuu24, vuu25, vuu26, vuu27, vuu28, False, vuu30, bb) → new_groupByZs01(vuu24, vuu25, vuu26, vuu27, vuu28, bb)
new_esEs22(vuu3002, vuu31002, app(ty_Ratio, bcd)) → new_esEs7(vuu3002, vuu31002, bcd)
new_esEs20(vuu3000, vuu31000, ty_Bool) → new_esEs11(vuu3000, vuu31000)
new_sr(Neg(vuu30000), Neg(vuu310000)) → Pos(new_primMulNat0(vuu30000, vuu310000))
new_esEs21(vuu3001, vuu31001, app(ty_[], bbe)) → new_esEs4(vuu3001, vuu31001, bbe)
new_esEs20(vuu3000, vuu31000, app(ty_Maybe, bag)) → new_esEs5(vuu3000, vuu31000, bag)
new_esEs5(Just(vuu3000), Just(vuu31000), app(ty_[], dd)) → new_esEs4(vuu3000, vuu31000, dd)
new_sr(Pos(vuu30000), Pos(vuu310000)) → Pos(new_primMulNat0(vuu30000, vuu310000))
new_asAs(False, vuu37) → False
new_esEs7(:%(vuu3000, vuu3001), :%(vuu31000, vuu31001), hb) → new_asAs(new_esEs24(vuu3000, vuu31000, hb), new_esEs25(vuu3001, vuu31001, hb))
new_groupByZs0([], :(:(vuu3100, vuu3101), vuu311), ba) → :(:(vuu3100, vuu3101), vuu311)
new_primEqNat0(Zero, Zero) → True
new_primMulNat0(Zero, Succ(vuu3100000)) → Zero
new_primMulNat0(Succ(vuu300000), Zero) → Zero
new_esEs13(EQ, GT) → False
new_esEs13(GT, EQ) → False
new_esEs13(LT, GT) → False
new_esEs13(GT, LT) → False
new_esEs23(vuu3000, vuu31000, ty_Int) → new_esEs9(vuu3000, vuu31000)
new_span2Ys2(vuu11, vuu12, [], cf) → []
new_esEs18(vuu3000, vuu31000, app(ty_Maybe, fd)) → new_esEs5(vuu3000, vuu31000, fd)
new_esEs18(vuu3000, vuu31000, app(ty_[], eh)) → new_esEs4(vuu3000, vuu31000, eh)
new_esEs11(True, True) → True
new_esEs8(Right(vuu3000), Right(vuu31000), hc, app(ty_Maybe, bfg)) → new_esEs5(vuu3000, vuu31000, bfg)
new_esEs23(vuu3000, vuu31000, app(ty_Maybe, cc)) → new_esEs5(vuu3000, vuu31000, cc)
new_esEs8(Left(vuu3000), Left(vuu31000), app(ty_Ratio, bdf), hd) → new_esEs7(vuu3000, vuu31000, bdf)
new_esEs5(Just(vuu3000), Just(vuu31000), app(app(ty_@2, ea), eb)) → new_esEs15(vuu3000, vuu31000, ea, eb)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Bool, hd) → new_esEs11(vuu3000, vuu31000)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Ordering, hd) → new_esEs13(vuu3000, vuu31000)
new_primPlusNat0(Succ(vuu490), vuu3100000) → Succ(Succ(new_primPlusNat1(vuu490, vuu3100000)))
new_esEs8(Left(vuu3000), Left(vuu31000), app(app(ty_@2, bef), beg), hd) → new_esEs15(vuu3000, vuu31000, bef, beg)
new_esEs26(vuu300, vuu3100, app(ty_[], bc)) → new_esEs4(vuu300, vuu3100, bc)
new_span2Ys2(vuu11, vuu12, :(vuu150, vuu151), cf) → new_span2Ys11(vuu11, vuu12, vuu150, vuu151, new_esEs4(:(vuu11, vuu12), vuu150, cf), cf)
new_span2Ys11(vuu11, vuu12, vuu150, vuu151, True, cf) → new_span2Ys12(vuu11, vuu12, vuu150, vuu151, new_span2Ys2(vuu11, vuu12, vuu151, cf), new_span2Zs2(vuu11, vuu12, vuu151, cf), cf)
new_esEs5(Just(vuu3000), Just(vuu31000), app(app(ty_Either, db), dc)) → new_esEs8(vuu3000, vuu31000, db, dc)
new_esEs5(Nothing, Just(vuu31000), cg) → False
new_esEs5(Just(vuu3000), Nothing, cg) → False
new_esEs19(vuu3001, vuu31001, ty_Integer) → new_esEs16(vuu3001, vuu31001)
new_esEs19(vuu3001, vuu31001, ty_Char) → new_esEs6(vuu3001, vuu31001)
new_primEqInt(Neg(Succ(vuu30000)), Neg(Succ(vuu310000))) → new_primEqNat0(vuu30000, vuu310000)
new_esEs4([], [], bc) → True
new_esEs20(vuu3000, vuu31000, ty_Float) → new_esEs17(vuu3000, vuu31000)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_@0, hd) → new_esEs10(vuu3000, vuu31000)
new_esEs18(vuu3000, vuu31000, ty_@0) → new_esEs10(vuu3000, vuu31000)
new_span2Zs2(vuu24, vuu25, [], bb) → []
new_primPlusNat1(Succ(vuu4900), Zero) → Succ(vuu4900)
new_primPlusNat1(Zero, Succ(vuu31000000)) → Succ(vuu31000000)
new_esEs23(vuu3000, vuu31000, app(ty_Ratio, bd)) → new_esEs7(vuu3000, vuu31000, bd)
new_esEs18(vuu3000, vuu31000, app(ty_Ratio, ee)) → new_esEs7(vuu3000, vuu31000, ee)
new_esEs8(Left(vuu3000), Right(vuu31000), hc, hd) → False
new_esEs8(Right(vuu3000), Left(vuu31000), hc, hd) → False
new_esEs8(Right(vuu3000), Right(vuu31000), hc, app(app(ty_Either, bfa), bfb)) → new_esEs8(vuu3000, vuu31000, bfa, bfb)
new_esEs6(Char(vuu3000), Char(vuu31000)) → new_primEqNat0(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, app(app(ty_Either, baa), bab)) → new_esEs8(vuu3000, vuu31000, baa, bab)
new_span2Zs11(vuu24, vuu25, vuu280, vuu281, False, bb) → :(vuu280, vuu281)
new_esEs21(vuu3001, vuu31001, ty_Double) → new_esEs14(vuu3001, vuu31001)
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Float) → new_esEs17(vuu3000, vuu31000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs18(vuu3000, vuu31000, ty_Float) → new_esEs17(vuu3000, vuu31000)
new_esEs5(Nothing, Nothing, cg) → True
new_groupByZs00(vuu24, vuu25, vuu26, vuu27, vuu28, True, False, bb) → new_groupByZs01(vuu24, vuu25, vuu26, vuu27, vuu28, bb)
new_span2Zs3([], ba) → []
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs18(vuu3000, vuu31000, ty_Bool) → new_esEs11(vuu3000, vuu31000)
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Char) → new_esEs6(vuu3000, vuu31000)
new_esEs22(vuu3002, vuu31002, ty_Integer) → new_esEs16(vuu3002, vuu31002)
new_primEqInt(Neg(Succ(vuu30000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(vuu310000))) → False
new_groupByZs02(vuu24, vuu25, vuu26, vuu27, vuu28, vuu38, bb) → new_span2Zs2(vuu24, vuu25, vuu28, bb)
new_esEs26(vuu300, vuu3100, ty_Char) → new_esEs6(vuu300, vuu3100)
new_esEs23(vuu3000, vuu31000, ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, ty_@0) → new_esEs10(vuu3000, vuu31000)
new_esEs4(:(vuu3000, vuu3001), [], bc) → False
new_esEs4([], :(vuu31000, vuu31001), bc) → False
new_span2Zs13(vuu3110, vuu3111, vuu45, vuu44, ba) → vuu44
new_esEs20(vuu3000, vuu31000, ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs22(vuu3002, vuu31002, app(ty_Maybe, bdc)) → new_esEs5(vuu3002, vuu31002, bdc)
new_esEs21(vuu3001, vuu31001, app(ty_Maybe, bca)) → new_esEs5(vuu3001, vuu31001, bca)
new_esEs21(vuu3001, vuu31001, ty_Float) → new_esEs17(vuu3001, vuu31001)
new_primPlusNat1(Zero, Zero) → Zero
new_span2Zs2(vuu24, vuu25, :(vuu280, vuu281), bb) → new_span2Zs11(vuu24, vuu25, vuu280, vuu281, new_esEs4(:(vuu24, vuu25), vuu280, bb), bb)
new_asAs(True, vuu37) → vuu37
new_esEs5(Just(vuu3000), Just(vuu31000), ty_@0) → new_esEs10(vuu3000, vuu31000)
new_primMulNat0(Succ(vuu300000), Succ(vuu3100000)) → new_primPlusNat0(new_primMulNat0(vuu300000, Succ(vuu3100000)), vuu3100000)
new_esEs26(vuu300, vuu3100, ty_Integer) → new_esEs16(vuu300, vuu3100)
new_esEs19(vuu3001, vuu31001, app(ty_[], gc)) → new_esEs4(vuu3001, vuu31001, gc)
new_esEs8(Right(vuu3000), Right(vuu31000), hc, ty_Int) → new_esEs9(vuu3000, vuu31000)
new_esEs18(vuu3000, vuu31000, ty_Double) → new_esEs14(vuu3000, vuu31000)
new_esEs13(LT, LT) → True
new_esEs22(vuu3002, vuu31002, app(ty_[], bcg)) → new_esEs4(vuu3002, vuu31002, bcg)
new_esEs11(False, False) → True
new_span2Ys3(:(vuu3110, vuu3111), ba) → new_span2Ys13(vuu3110, vuu3111, new_esEs4([], vuu3110, ba), ba)
new_primEqInt(Pos(Succ(vuu30000)), Pos(Succ(vuu310000))) → new_primEqNat0(vuu30000, vuu310000)
new_esEs8(Right(vuu3000), Right(vuu31000), hc, ty_Char) → new_esEs6(vuu3000, vuu31000)
new_span2Ys11(vuu11, vuu12, vuu150, vuu151, False, cf) → []
new_esEs8(Right(vuu3000), Right(vuu31000), hc, ty_Float) → new_esEs17(vuu3000, vuu31000)
new_esEs22(vuu3002, vuu31002, app(app(ty_Either, bce), bcf)) → new_esEs8(vuu3002, vuu31002, bce, bcf)
new_esEs19(vuu3001, vuu31001, ty_@0) → new_esEs10(vuu3001, vuu31001)
new_span2Ys3([], ba) → []
new_esEs25(vuu3001, vuu31001, ty_Int) → new_esEs9(vuu3001, vuu31001)
new_groupByZs0([], :([], vuu311), ba) → new_span2Zs3(vuu311, ba)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Integer, hd) → new_esEs16(vuu3000, vuu31000)
new_esEs8(Left(vuu3000), Left(vuu31000), app(app(app(ty_@3, beb), bec), bed), hd) → new_esEs12(vuu3000, vuu31000, beb, bec, bed)
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Bool) → new_esEs11(vuu3000, vuu31000)
new_primEqNat0(Succ(vuu30000), Succ(vuu310000)) → new_primEqNat0(vuu30000, vuu310000)
new_esEs8(Right(vuu3000), Right(vuu31000), hc, ty_Bool) → new_esEs11(vuu3000, vuu31000)
new_esEs9(vuu300, vuu3100) → new_primEqInt(vuu300, vuu3100)
new_esEs20(vuu3000, vuu31000, ty_Double) → new_esEs14(vuu3000, vuu31000)
new_esEs8(Left(vuu3000), Left(vuu31000), app(ty_Maybe, bee), hd) → new_esEs5(vuu3000, vuu31000, bee)
new_span2Zs3(:(vuu3110, vuu3111), ba) → new_span2Zs12(vuu3110, vuu3111, new_esEs4([], vuu3110, ba), ba)
new_esEs8(Right(vuu3000), Right(vuu31000), hc, app(ty_Ratio, beh)) → new_esEs7(vuu3000, vuu31000, beh)
new_esEs21(vuu3001, vuu31001, app(ty_Ratio, bbb)) → new_esEs7(vuu3001, vuu31001, bbb)
new_esEs23(vuu3000, vuu31000, app(app(ty_@2, cd), ce)) → new_esEs15(vuu3000, vuu31000, cd, ce)
new_esEs26(vuu300, vuu3100, ty_Ordering) → new_esEs13(vuu300, vuu3100)
new_primEqInt(Pos(Zero), Pos(Succ(vuu310000))) → False
new_primEqInt(Pos(Succ(vuu30000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_span2Zs11(vuu24, vuu25, vuu280, vuu281, True, bb) → new_span2Zs14(vuu24, vuu25, vuu280, vuu281, new_span2Ys2(vuu24, vuu25, vuu281, bb), new_span2Zs2(vuu24, vuu25, vuu281, bb), bb)
new_esEs23(vuu3000, vuu31000, ty_Ordering) → new_esEs13(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, app(ty_[], bg)) → new_esEs4(vuu3000, vuu31000, bg)
new_esEs21(vuu3001, vuu31001, ty_Char) → new_esEs6(vuu3001, vuu31001)
The set Q consists of the following terms:
new_esEs10(@0, @0)
new_esEs8(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs22(x0, x1, ty_Integer)
new_groupByZs00(x0, x1, x2, x3, x4, False, x5, x6)
new_esEs5(Just(x0), Just(x1), app(ty_Ratio, x2))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_span2Zs12(x0, x1, True, x2)
new_esEs18(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_span2Ys2(x0, x1, :(x2, x3), x4)
new_esEs8(Left(x0), Left(x1), ty_Int, x2)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_groupByZs0(:(x0, x1), :([], x2), x3)
new_groupByZs01(x0, x1, x2, x3, x4, x5)
new_esEs11(True, True)
new_esEs5(Just(x0), Just(x1), ty_Float)
new_esEs5(Just(x0), Just(x1), ty_Bool)
new_esEs4([], [], x0)
new_groupByZs02(x0, x1, x2, x3, x4, x5, x6)
new_primEqNat0(Zero, Succ(x0))
new_esEs8(Left(x0), Left(x1), ty_Double, x2)
new_esEs26(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Float)
new_span2Zs11(x0, x1, x2, x3, False, x4)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs18(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Int)
new_esEs8(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs23(x0, x1, ty_Char)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Float)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_@0)
new_groupByZs0(x0, [], x1)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs5(Just(x0), Just(x1), ty_Integer)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, app(app(ty_@2, x2), x3))
new_span2Ys3(:(x0, x1), x2)
new_esEs5(Just(x0), Just(x1), ty_Int)
new_esEs13(GT, GT)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs8(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs21(x0, x1, ty_Integer)
new_span2Zs12(x0, x1, False, x2)
new_span2Ys13(x0, x1, False, x2)
new_esEs18(x0, x1, ty_Bool)
new_esEs15(@2(x0, x1), @2(x2, x3), x4, x5)
new_primEqInt(Neg(Zero), Neg(Zero))
new_span2Ys14(x0, x1, x2, x3, x4)
new_esEs20(x0, x1, ty_Char)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs8(Left(x0), Left(x1), ty_Bool, x2)
new_esEs20(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Bool)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_Int)
new_esEs5(Just(x0), Nothing, x1)
new_esEs19(x0, x1, ty_Int)
new_esEs8(Right(x0), Right(x1), x2, ty_Int)
new_esEs11(True, False)
new_esEs11(False, True)
new_esEs8(Right(x0), Left(x1), x2, x3)
new_esEs8(Left(x0), Right(x1), x2, x3)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(Left(x0), Left(x1), ty_Float, x2)
new_primMulNat0(Succ(x0), Zero)
new_esEs8(Right(x0), Right(x1), x2, ty_Bool)
new_sr(Pos(x0), Pos(x1))
new_esEs6(Char(x0), Char(x1))
new_esEs18(x0, x1, app(app(ty_@2, x2), x3))
new_groupByZs0([], :([], x0), x1)
new_esEs4([], :(x0, x1), x2)
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_Char)
new_span2Ys2(x0, x1, [], x2)
new_span2Zs2(x0, x1, [], x2)
new_esEs8(Right(x0), Right(x1), x2, ty_Double)
new_esEs5(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs19(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Integer)
new_esEs26(x0, x1, ty_Double)
new_esEs18(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(Nothing, Nothing, x0)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs8(Right(x0), Right(x1), x2, ty_@0)
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_esEs8(Left(x0), Left(x1), ty_@0, x2)
new_esEs21(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Bool)
new_esEs13(GT, LT)
new_esEs13(LT, GT)
new_esEs5(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_span2Zs2(x0, x1, :(x2, x3), x4)
new_span2Ys12(x0, x1, x2, x3, x4, x5, x6)
new_esEs19(x0, x1, ty_Float)
new_esEs18(x0, x1, ty_Float)
new_esEs23(x0, x1, ty_@0)
new_sr(Neg(x0), Neg(x1))
new_esEs5(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs8(Right(x0), Right(x1), x2, ty_Float)
new_esEs26(x0, x1, app(ty_[], x2))
new_primEqNat0(Zero, Zero)
new_esEs8(Right(x0), Right(x1), x2, ty_Integer)
new_esEs14(Double(x0, x1), Double(x2, x3))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs19(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_@0)
new_esEs8(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs13(GT, EQ)
new_esEs13(EQ, GT)
new_esEs8(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs13(LT, LT)
new_esEs21(x0, x1, ty_Float)
new_esEs19(x0, x1, app(app(ty_Either, x2), x3))
new_span2Zs14(x0, x1, x2, x3, x4, x5, x6)
new_esEs24(x0, x1, ty_Integer)
new_span2Zs3([], x0)
new_primMulNat0(Zero, Zero)
new_span2Ys13(x0, x1, True, x2)
new_span2Ys3([], x0)
new_esEs5(Just(x0), Just(x1), ty_Ordering)
new_esEs8(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs8(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs19(x0, x1, ty_Bool)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_span2Zs13(x0, x1, x2, x3, x4)
new_esEs5(Just(x0), Just(x1), ty_@0)
new_esEs21(x0, x1, ty_Ordering)
new_esEs18(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Bool)
new_groupByZs0([], :(:(x0, x1), x2), x3)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Int)
new_esEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(LT, EQ)
new_esEs13(EQ, LT)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs5(Nothing, Just(x0), x1)
new_primEqNat0(Succ(x0), Zero)
new_span2Zs11(x0, x1, x2, x3, True, x4)
new_esEs19(x0, x1, ty_@0)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_span2Ys11(x0, x1, x2, x3, False, x4)
new_esEs13(EQ, EQ)
new_esEs23(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Double)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs7(:%(x0, x1), :%(x2, x3), x4)
new_esEs26(x0, x1, ty_Float)
new_esEs21(x0, x1, ty_Bool)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, ty_Ordering)
new_primMulNat0(Succ(x0), Succ(x1))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_asAs(True, x0)
new_esEs8(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs18(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Succ(x0))
new_esEs19(x0, x1, ty_Double)
new_primPlusNat1(Succ(x0), Zero)
new_esEs8(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs26(x0, x1, ty_@0)
new_esEs8(Right(x0), Right(x1), x2, ty_Char)
new_esEs23(x0, x1, ty_Double)
new_esEs8(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs4(:(x0, x1), [], x2)
new_esEs4(:(x0, x1), :(x2, x3), x4)
new_esEs5(Just(x0), Just(x1), ty_Char)
new_esEs5(Just(x0), Just(x1), app(ty_[], x2))
new_esEs11(False, False)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs8(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs20(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Char)
new_esEs17(Float(x0, x1), Float(x2, x3))
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs18(x0, x1, ty_@0)
new_groupByZs00(x0, x1, x2, x3, x4, True, False, x5)
new_groupByZs0(:(x0, x1), :(:(x2, x3), x4), x5)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Char)
new_esEs19(x0, x1, app(ty_[], x2))
new_esEs8(Left(x0), Left(x1), ty_Char, x2)
new_esEs16(Integer(x0), Integer(x1))
new_primMulNat0(Zero, Succ(x0))
new_esEs20(x0, x1, ty_Double)
new_span2Zs3(:(x0, x1), x2)
new_primPlusNat1(Zero, Zero)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs23(x0, x1, ty_Float)
new_span2Ys11(x0, x1, x2, x3, True, x4)
new_primPlusNat0(Succ(x0), x1)
new_esEs18(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_groupByZs00(x0, x1, x2, x3, x4, True, True, x5)
new_esEs8(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs18(x0, x1, ty_Int)
new_asAs(False, x0)
new_esEs18(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs23(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Char)
new_esEs18(x0, x1, ty_Char)
new_esEs5(Just(x0), Just(x1), ty_Double)
new_primPlusNat0(Zero, x0)
new_esEs20(x0, x1, ty_Ordering)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs8(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs5(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs12(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(x0, x1)
new_esEs25(x0, x1, ty_Int)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs8(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs18(x0, x1, ty_Ordering)
new_esEs20(x0, x1, ty_Int)
new_esEs19(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_Int)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(x0, x1, app(ty_Maybe, x2))
new_esEs8(Left(x0), Left(x1), ty_Integer, x2)
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].
The following pairs can be oriented strictly and are deleted.
new_groupBy(:(vuu30, vuu31), ba) → new_groupBy(new_groupByZs0(vuu30, vuu31, ba), ba)
The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25]:
POL(:(x1, x2)) = 1 + x2
POL(:%(x1, x2)) = 0
POL(@0) = 0
POL(@2(x1, x2)) = 0
POL(@3(x1, x2, x3)) = 0
POL(Char(x1)) = 0
POL(Double(x1, x2)) = 0
POL(EQ) = 0
POL(False) = 0
POL(Float(x1, x2)) = 0
POL(GT) = 0
POL(Integer(x1)) = 0
POL(Just(x1)) = 0
POL(LT) = 0
POL(Left(x1)) = 0
POL(Neg(x1)) = 0
POL(Nothing) = 0
POL(Pos(x1)) = 1
POL(Right(x1)) = 0
POL(Succ(x1)) = 0
POL(True) = 0
POL(Zero) = 1
POL([]) = 0
POL(app(x1, x2)) = 0
POL(new_asAs(x1, x2)) = 0
POL(new_esEs10(x1, x2)) = 0
POL(new_esEs11(x1, x2)) = 0
POL(new_esEs12(x1, x2, x3, x4, x5)) = 0
POL(new_esEs13(x1, x2)) = 0
POL(new_esEs14(x1, x2)) = 0
POL(new_esEs15(x1, x2, x3, x4)) = 0
POL(new_esEs16(x1, x2)) = 0
POL(new_esEs17(x1, x2)) = 0
POL(new_esEs18(x1, x2, x3)) = 0
POL(new_esEs19(x1, x2, x3)) = 0
POL(new_esEs20(x1, x2, x3)) = 0
POL(new_esEs21(x1, x2, x3)) = 0
POL(new_esEs22(x1, x2, x3)) = 0
POL(new_esEs23(x1, x2, x3)) = 0
POL(new_esEs24(x1, x2, x3)) = 0
POL(new_esEs25(x1, x2, x3)) = 0
POL(new_esEs26(x1, x2, x3)) = 0
POL(new_esEs4(x1, x2, x3)) = 0
POL(new_esEs5(x1, x2, x3)) = 0
POL(new_esEs6(x1, x2)) = 0
POL(new_esEs7(x1, x2, x3)) = 0
POL(new_esEs8(x1, x2, x3, x4)) = 0
POL(new_esEs9(x1, x2)) = 0
POL(new_groupBy(x1, x2)) = x1
POL(new_groupByZs0(x1, x2, x3)) = x2
POL(new_groupByZs00(x1, x2, x3, x4, x5, x6, x7, x8)) = 1 + x5
POL(new_groupByZs01(x1, x2, x3, x4, x5, x6)) = 1 + x5
POL(new_groupByZs02(x1, x2, x3, x4, x5, x6, x7)) = 1 + x5
POL(new_primEqInt(x1, x2)) = 0
POL(new_primEqNat0(x1, x2)) = 0
POL(new_primMulNat0(x1, x2)) = 1 + x1 + x2
POL(new_primPlusNat0(x1, x2)) = 0
POL(new_primPlusNat1(x1, x2)) = 0
POL(new_span2Ys11(x1, x2, x3, x4, x5, x6)) = 1 + x4
POL(new_span2Ys12(x1, x2, x3, x4, x5, x6, x7)) = 1 + x5
POL(new_span2Ys13(x1, x2, x3, x4)) = 1 + x2
POL(new_span2Ys14(x1, x2, x3, x4, x5)) = 1 + x3
POL(new_span2Ys2(x1, x2, x3, x4)) = x3
POL(new_span2Ys3(x1, x2)) = x1
POL(new_span2Zs11(x1, x2, x3, x4, x5, x6)) = 1 + x4
POL(new_span2Zs12(x1, x2, x3, x4)) = 1 + x2
POL(new_span2Zs13(x1, x2, x3, x4, x5)) = x4
POL(new_span2Zs14(x1, x2, x3, x4, x5, x6, x7)) = x6
POL(new_span2Zs2(x1, x2, x3, x4)) = x3
POL(new_span2Zs3(x1, x2)) = x1
POL(new_sr(x1, x2)) = 1 + x1
POL(ty_@0) = 0
POL(ty_@2) = 0
POL(ty_@3) = 0
POL(ty_Bool) = 0
POL(ty_Char) = 0
POL(ty_Double) = 0
POL(ty_Either) = 0
POL(ty_Float) = 0
POL(ty_Int) = 0
POL(ty_Integer) = 0
POL(ty_Maybe) = 0
POL(ty_Ordering) = 0
POL(ty_Ratio) = 0
POL(ty_[]) = 0
The following usable rules [17] were oriented:
new_groupByZs01(vuu24, vuu25, vuu26, vuu27, vuu28, bb) → :(:(vuu26, vuu27), vuu28)
new_groupByZs0([], :([], vuu311), ba) → new_span2Zs3(vuu311, ba)
new_span2Zs11(vuu24, vuu25, vuu280, vuu281, True, bb) → new_span2Zs14(vuu24, vuu25, vuu280, vuu281, new_span2Ys2(vuu24, vuu25, vuu281, bb), new_span2Zs2(vuu24, vuu25, vuu281, bb), bb)
new_span2Ys3([], ba) → []
new_groupByZs00(vuu24, vuu25, vuu26, vuu27, vuu28, False, vuu30, bb) → new_groupByZs01(vuu24, vuu25, vuu26, vuu27, vuu28, bb)
new_span2Ys3(:(vuu3110, vuu3111), ba) → new_span2Ys13(vuu3110, vuu3111, new_esEs4([], vuu3110, ba), ba)
new_span2Zs12(vuu3110, vuu3111, True, ba) → new_span2Zs13(vuu3110, vuu3111, new_span2Ys3(vuu3111, ba), new_span2Zs3(vuu3111, ba), ba)
new_groupByZs0([], :(:(vuu3100, vuu3101), vuu311), ba) → :(:(vuu3100, vuu3101), vuu311)
new_span2Ys11(vuu11, vuu12, vuu150, vuu151, False, cf) → []
new_span2Ys13(vuu3110, vuu3111, False, ba) → []
new_span2Ys11(vuu11, vuu12, vuu150, vuu151, True, cf) → new_span2Ys12(vuu11, vuu12, vuu150, vuu151, new_span2Ys2(vuu11, vuu12, vuu151, cf), new_span2Zs2(vuu11, vuu12, vuu151, cf), cf)
new_span2Zs2(vuu24, vuu25, [], bb) → []
new_span2Zs3(:(vuu3110, vuu3111), ba) → new_span2Zs12(vuu3110, vuu3111, new_esEs4([], vuu3110, ba), ba)
new_span2Ys12(vuu11, vuu12, vuu150, vuu151, vuu47, vuu46, cf) → :(vuu150, vuu47)
new_span2Ys2(vuu11, vuu12, [], cf) → []
new_groupByZs00(vuu24, vuu25, vuu26, vuu27, vuu28, True, True, bb) → new_groupByZs02(vuu24, vuu25, vuu26, vuu27, vuu28, new_span2Ys2(vuu24, vuu25, vuu28, bb), bb)
new_groupByZs0(:(vuu300, vuu301), :([], vuu311), ba) → :([], vuu311)
new_span2Zs3([], ba) → []
new_span2Zs11(vuu24, vuu25, vuu280, vuu281, False, bb) → :(vuu280, vuu281)
new_groupByZs02(vuu24, vuu25, vuu26, vuu27, vuu28, vuu38, bb) → new_span2Zs2(vuu24, vuu25, vuu28, bb)
new_span2Ys13(vuu3110, vuu3111, True, ba) → new_span2Ys14(vuu3110, vuu3111, new_span2Ys3(vuu3111, ba), new_span2Zs3(vuu3111, ba), ba)
new_span2Zs12(vuu3110, vuu3111, False, ba) → :(vuu3110, vuu3111)
new_span2Ys2(vuu11, vuu12, :(vuu150, vuu151), cf) → new_span2Ys11(vuu11, vuu12, vuu150, vuu151, new_esEs4(:(vuu11, vuu12), vuu150, cf), cf)
new_span2Zs14(vuu24, vuu25, vuu280, vuu281, vuu51, vuu50, bb) → vuu50
new_groupByZs0(vuu30, [], ba) → []
new_span2Ys14(vuu3110, vuu3111, vuu43, vuu42, ba) → :(vuu3110, vuu43)
new_groupByZs0(:(vuu300, vuu301), :(:(vuu3100, vuu3101), vuu311), ba) → new_groupByZs00(vuu300, vuu301, vuu3100, vuu3101, vuu311, new_esEs26(vuu300, vuu3100, ba), new_esEs4(vuu301, vuu3101, ba), ba)
new_groupByZs00(vuu24, vuu25, vuu26, vuu27, vuu28, True, False, bb) → new_groupByZs01(vuu24, vuu25, vuu26, vuu27, vuu28, bb)
new_span2Zs13(vuu3110, vuu3111, vuu45, vuu44, ba) → vuu44
new_span2Zs2(vuu24, vuu25, :(vuu280, vuu281), bb) → new_span2Zs11(vuu24, vuu25, vuu280, vuu281, new_esEs4(:(vuu24, vuu25), vuu280, bb), bb)
↳ HASKELL
↳ LR
↳ HASKELL
↳ BR
↳ HASKELL
↳ COR
↳ HASKELL
↳ LetRed
↳ HASKELL
↳ Narrow
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
Q DP problem:
P is empty.
The TRS R consists of the following rules:
new_esEs22(vuu3002, vuu31002, app(app(ty_@2, bdd), bde)) → new_esEs15(vuu3002, vuu31002, bdd, bde)
new_esEs23(vuu3000, vuu31000, ty_Char) → new_esEs6(vuu3000, vuu31000)
new_esEs8(Right(vuu3000), Right(vuu31000), hc, ty_Double) → new_esEs14(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, app(ty_Ratio, hh)) → new_esEs7(vuu3000, vuu31000, hh)
new_esEs8(Right(vuu3000), Right(vuu31000), hc, app(ty_[], bfc)) → new_esEs4(vuu3000, vuu31000, bfc)
new_esEs26(vuu300, vuu3100, app(app(app(ty_@3, he), hf), hg)) → new_esEs12(vuu300, vuu3100, he, hf, hg)
new_primPlusNat1(Succ(vuu4900), Succ(vuu31000000)) → Succ(Succ(new_primPlusNat1(vuu4900, vuu31000000)))
new_esEs19(vuu3001, vuu31001, app(ty_Ratio, fh)) → new_esEs7(vuu3001, vuu31001, fh)
new_primEqInt(Pos(Succ(vuu30000)), Neg(vuu31000)) → False
new_primEqInt(Neg(Succ(vuu30000)), Pos(vuu31000)) → False
new_esEs18(vuu3000, vuu31000, ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs19(vuu3001, vuu31001, ty_Bool) → new_esEs11(vuu3001, vuu31001)
new_esEs8(Left(vuu3000), Left(vuu31000), app(ty_[], bea), hd) → new_esEs4(vuu3000, vuu31000, bea)
new_esEs26(vuu300, vuu3100, ty_Double) → new_esEs14(vuu300, vuu3100)
new_esEs26(vuu300, vuu3100, ty_Int) → new_esEs9(vuu300, vuu3100)
new_primEqInt(Pos(Zero), Neg(Succ(vuu310000))) → False
new_primEqInt(Neg(Zero), Pos(Succ(vuu310000))) → False
new_span2Zs12(vuu3110, vuu3111, True, ba) → new_span2Zs13(vuu3110, vuu3111, new_span2Ys3(vuu3111, ba), new_span2Zs3(vuu3111, ba), ba)
new_esEs8(Right(vuu3000), Right(vuu31000), hc, ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, ty_Int) → new_esEs9(vuu3000, vuu31000)
new_span2Zs12(vuu3110, vuu3111, False, ba) → :(vuu3110, vuu3111)
new_esEs23(vuu3000, vuu31000, ty_Bool) → new_esEs11(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, app(app(ty_@2, bah), bba)) → new_esEs15(vuu3000, vuu31000, bah, bba)
new_esEs23(vuu3000, vuu31000, ty_Float) → new_esEs17(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, ty_Float) → new_esEs17(vuu300, vuu3100)
new_esEs26(vuu300, vuu3100, app(app(ty_@2, ec), ed)) → new_esEs15(vuu300, vuu3100, ec, ed)
new_esEs19(vuu3001, vuu31001, ty_Ordering) → new_esEs13(vuu3001, vuu31001)
new_primMulNat0(Zero, Zero) → Zero
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Double) → new_esEs14(vuu3000, vuu31000)
new_esEs15(@2(vuu3000, vuu3001), @2(vuu31000, vuu31001), ec, ed) → new_asAs(new_esEs18(vuu3000, vuu31000, ec), new_esEs19(vuu3001, vuu31001, ed))
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Int) → new_esEs9(vuu3000, vuu31000)
new_span2Ys14(vuu3110, vuu3111, vuu43, vuu42, ba) → :(vuu3110, vuu43)
new_esEs21(vuu3001, vuu31001, app(app(ty_Either, bbc), bbd)) → new_esEs8(vuu3001, vuu31001, bbc, bbd)
new_esEs26(vuu300, vuu3100, app(ty_Ratio, hb)) → new_esEs7(vuu300, vuu3100, hb)
new_esEs23(vuu3000, vuu31000, app(app(app(ty_@3, bh), ca), cb)) → new_esEs12(vuu3000, vuu31000, bh, ca, cb)
new_primPlusNat0(Zero, vuu3100000) → Succ(vuu3100000)
new_esEs21(vuu3001, vuu31001, app(app(ty_@2, bcb), bcc)) → new_esEs15(vuu3001, vuu31001, bcb, bcc)
new_esEs20(vuu3000, vuu31000, app(app(app(ty_@3, bad), bae), baf)) → new_esEs12(vuu3000, vuu31000, bad, bae, baf)
new_esEs12(@3(vuu3000, vuu3001, vuu3002), @3(vuu31000, vuu31001, vuu31002), he, hf, hg) → new_asAs(new_esEs20(vuu3000, vuu31000, he), new_asAs(new_esEs21(vuu3001, vuu31001, hf), new_esEs22(vuu3002, vuu31002, hg)))
new_esEs13(EQ, EQ) → True
new_sr(Neg(vuu30000), Pos(vuu310000)) → Neg(new_primMulNat0(vuu30000, vuu310000))
new_sr(Pos(vuu30000), Neg(vuu310000)) → Neg(new_primMulNat0(vuu30000, vuu310000))
new_esEs19(vuu3001, vuu31001, ty_Int) → new_esEs9(vuu3001, vuu31001)
new_span2Zs14(vuu24, vuu25, vuu280, vuu281, vuu51, vuu50, bb) → vuu50
new_esEs23(vuu3000, vuu31000, ty_@0) → new_esEs10(vuu3000, vuu31000)
new_esEs4(:(vuu3000, vuu3001), :(vuu31000, vuu31001), bc) → new_asAs(new_esEs23(vuu3000, vuu31000, bc), new_esEs4(vuu3001, vuu31001, bc))
new_span2Ys13(vuu3110, vuu3111, True, ba) → new_span2Ys14(vuu3110, vuu3111, new_span2Ys3(vuu3111, ba), new_span2Zs3(vuu3111, ba), ba)
new_esEs22(vuu3002, vuu31002, ty_Bool) → new_esEs11(vuu3002, vuu31002)
new_groupByZs0(:(vuu300, vuu301), :([], vuu311), ba) → :([], vuu311)
new_esEs19(vuu3001, vuu31001, app(app(app(ty_@3, gd), ge), gf)) → new_esEs12(vuu3001, vuu31001, gd, ge, gf)
new_esEs21(vuu3001, vuu31001, ty_Integer) → new_esEs16(vuu3001, vuu31001)
new_esEs18(vuu3000, vuu31000, ty_Ordering) → new_esEs13(vuu3000, vuu31000)
new_esEs5(Just(vuu3000), Just(vuu31000), app(ty_Maybe, dh)) → new_esEs5(vuu3000, vuu31000, dh)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Float, hd) → new_esEs17(vuu3000, vuu31000)
new_esEs26(vuu300, vuu3100, ty_@0) → new_esEs10(vuu300, vuu3100)
new_esEs24(vuu3000, vuu31000, ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs18(vuu3000, vuu31000, ty_Int) → new_esEs9(vuu3000, vuu31000)
new_esEs18(vuu3000, vuu31000, ty_Char) → new_esEs6(vuu3000, vuu31000)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Double, hd) → new_esEs14(vuu3000, vuu31000)
new_esEs8(Right(vuu3000), Right(vuu31000), hc, ty_@0) → new_esEs10(vuu3000, vuu31000)
new_esEs13(GT, GT) → True
new_esEs8(Right(vuu3000), Right(vuu31000), hc, ty_Ordering) → new_esEs13(vuu3000, vuu31000)
new_primEqNat0(Zero, Succ(vuu310000)) → False
new_primEqNat0(Succ(vuu30000), Zero) → False
new_esEs22(vuu3002, vuu31002, ty_Float) → new_esEs17(vuu3002, vuu31002)
new_esEs21(vuu3001, vuu31001, ty_@0) → new_esEs10(vuu3001, vuu31001)
new_esEs21(vuu3001, vuu31001, ty_Int) → new_esEs9(vuu3001, vuu31001)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Int, hd) → new_esEs9(vuu3000, vuu31000)
new_esEs19(vuu3001, vuu31001, app(app(ty_@2, gh), ha)) → new_esEs15(vuu3001, vuu31001, gh, ha)
new_esEs22(vuu3002, vuu31002, ty_Char) → new_esEs6(vuu3002, vuu31002)
new_esEs17(Float(vuu3000, vuu3001), Float(vuu31000, vuu31001)) → new_esEs9(new_sr(vuu3000, vuu31000), new_sr(vuu3001, vuu31001))
new_esEs5(Just(vuu3000), Just(vuu31000), app(ty_Ratio, da)) → new_esEs7(vuu3000, vuu31000, da)
new_esEs22(vuu3002, vuu31002, ty_Double) → new_esEs14(vuu3002, vuu31002)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_span2Ys13(vuu3110, vuu3111, False, ba) → []
new_esEs13(LT, EQ) → False
new_esEs13(EQ, LT) → False
new_esEs20(vuu3000, vuu31000, ty_Ordering) → new_esEs13(vuu3000, vuu31000)
new_esEs14(Double(vuu3000, vuu3001), Double(vuu31000, vuu31001)) → new_esEs9(new_sr(vuu3000, vuu31000), new_sr(vuu3001, vuu31001))
new_esEs19(vuu3001, vuu31001, app(app(ty_Either, ga), gb)) → new_esEs8(vuu3001, vuu31001, ga, gb)
new_span2Ys12(vuu11, vuu12, vuu150, vuu151, vuu47, vuu46, cf) → :(vuu150, vuu47)
new_esEs22(vuu3002, vuu31002, ty_Ordering) → new_esEs13(vuu3002, vuu31002)
new_esEs22(vuu3002, vuu31002, ty_Int) → new_esEs9(vuu3002, vuu31002)
new_esEs18(vuu3000, vuu31000, app(app(app(ty_@3, fa), fb), fc)) → new_esEs12(vuu3000, vuu31000, fa, fb, fc)
new_esEs20(vuu3000, vuu31000, app(ty_[], bac)) → new_esEs4(vuu3000, vuu31000, bac)
new_esEs21(vuu3001, vuu31001, ty_Ordering) → new_esEs13(vuu3001, vuu31001)
new_esEs22(vuu3002, vuu31002, app(app(app(ty_@3, bch), bda), bdb)) → new_esEs12(vuu3002, vuu31002, bch, bda, bdb)
new_esEs21(vuu3001, vuu31001, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs12(vuu3001, vuu31001, bbf, bbg, bbh)
new_esEs19(vuu3001, vuu31001, app(ty_Maybe, gg)) → new_esEs5(vuu3001, vuu31001, gg)
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Ordering) → new_esEs13(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, app(app(ty_Either, be), bf)) → new_esEs8(vuu3000, vuu31000, be, bf)
new_esEs26(vuu300, vuu3100, app(ty_Maybe, cg)) → new_esEs5(vuu300, vuu3100, cg)
new_esEs22(vuu3002, vuu31002, ty_@0) → new_esEs10(vuu3002, vuu31002)
new_esEs26(vuu300, vuu3100, app(app(ty_Either, hc), hd)) → new_esEs8(vuu300, vuu3100, hc, hd)
new_esEs24(vuu3000, vuu31000, ty_Int) → new_esEs9(vuu3000, vuu31000)
new_esEs25(vuu3001, vuu31001, ty_Integer) → new_esEs16(vuu3001, vuu31001)
new_esEs5(Just(vuu3000), Just(vuu31000), app(app(app(ty_@3, de), df), dg)) → new_esEs12(vuu3000, vuu31000, de, df, dg)
new_groupByZs00(vuu24, vuu25, vuu26, vuu27, vuu28, True, True, bb) → new_groupByZs02(vuu24, vuu25, vuu26, vuu27, vuu28, new_span2Ys2(vuu24, vuu25, vuu28, bb), bb)
new_esEs18(vuu3000, vuu31000, app(app(ty_Either, ef), eg)) → new_esEs8(vuu3000, vuu31000, ef, eg)
new_groupByZs01(vuu24, vuu25, vuu26, vuu27, vuu28, bb) → :(:(vuu26, vuu27), vuu28)
new_esEs11(False, True) → False
new_esEs11(True, False) → False
new_esEs19(vuu3001, vuu31001, ty_Double) → new_esEs14(vuu3001, vuu31001)
new_esEs18(vuu3000, vuu31000, app(app(ty_@2, ff), fg)) → new_esEs15(vuu3000, vuu31000, ff, fg)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Char, hd) → new_esEs6(vuu3000, vuu31000)
new_esEs8(Right(vuu3000), Right(vuu31000), hc, app(app(ty_@2, bfh), bga)) → new_esEs15(vuu3000, vuu31000, bfh, bga)
new_esEs23(vuu3000, vuu31000, ty_Double) → new_esEs14(vuu3000, vuu31000)
new_esEs16(Integer(vuu3000), Integer(vuu31000)) → new_primEqInt(vuu3000, vuu31000)
new_esEs8(Left(vuu3000), Left(vuu31000), app(app(ty_Either, bdg), bdh), hd) → new_esEs8(vuu3000, vuu31000, bdg, bdh)
new_groupByZs0(:(vuu300, vuu301), :(:(vuu3100, vuu3101), vuu311), ba) → new_groupByZs00(vuu300, vuu301, vuu3100, vuu3101, vuu311, new_esEs26(vuu300, vuu3100, ba), new_esEs4(vuu301, vuu3101, ba), ba)
new_esEs8(Right(vuu3000), Right(vuu31000), hc, app(app(app(ty_@3, bfd), bfe), bff)) → new_esEs12(vuu3000, vuu31000, bfd, bfe, bff)
new_esEs21(vuu3001, vuu31001, ty_Bool) → new_esEs11(vuu3001, vuu31001)
new_esEs26(vuu300, vuu3100, ty_Bool) → new_esEs11(vuu300, vuu3100)
new_groupByZs0(vuu30, [], ba) → []
new_esEs20(vuu3000, vuu31000, ty_Char) → new_esEs6(vuu3000, vuu31000)
new_esEs19(vuu3001, vuu31001, ty_Float) → new_esEs17(vuu3001, vuu31001)
new_esEs10(@0, @0) → True
new_groupByZs00(vuu24, vuu25, vuu26, vuu27, vuu28, False, vuu30, bb) → new_groupByZs01(vuu24, vuu25, vuu26, vuu27, vuu28, bb)
new_esEs22(vuu3002, vuu31002, app(ty_Ratio, bcd)) → new_esEs7(vuu3002, vuu31002, bcd)
new_esEs20(vuu3000, vuu31000, ty_Bool) → new_esEs11(vuu3000, vuu31000)
new_sr(Neg(vuu30000), Neg(vuu310000)) → Pos(new_primMulNat0(vuu30000, vuu310000))
new_esEs21(vuu3001, vuu31001, app(ty_[], bbe)) → new_esEs4(vuu3001, vuu31001, bbe)
new_esEs20(vuu3000, vuu31000, app(ty_Maybe, bag)) → new_esEs5(vuu3000, vuu31000, bag)
new_esEs5(Just(vuu3000), Just(vuu31000), app(ty_[], dd)) → new_esEs4(vuu3000, vuu31000, dd)
new_sr(Pos(vuu30000), Pos(vuu310000)) → Pos(new_primMulNat0(vuu30000, vuu310000))
new_asAs(False, vuu37) → False
new_esEs7(:%(vuu3000, vuu3001), :%(vuu31000, vuu31001), hb) → new_asAs(new_esEs24(vuu3000, vuu31000, hb), new_esEs25(vuu3001, vuu31001, hb))
new_groupByZs0([], :(:(vuu3100, vuu3101), vuu311), ba) → :(:(vuu3100, vuu3101), vuu311)
new_primEqNat0(Zero, Zero) → True
new_primMulNat0(Zero, Succ(vuu3100000)) → Zero
new_primMulNat0(Succ(vuu300000), Zero) → Zero
new_esEs13(EQ, GT) → False
new_esEs13(GT, EQ) → False
new_esEs13(LT, GT) → False
new_esEs13(GT, LT) → False
new_esEs23(vuu3000, vuu31000, ty_Int) → new_esEs9(vuu3000, vuu31000)
new_span2Ys2(vuu11, vuu12, [], cf) → []
new_esEs18(vuu3000, vuu31000, app(ty_Maybe, fd)) → new_esEs5(vuu3000, vuu31000, fd)
new_esEs18(vuu3000, vuu31000, app(ty_[], eh)) → new_esEs4(vuu3000, vuu31000, eh)
new_esEs11(True, True) → True
new_esEs8(Right(vuu3000), Right(vuu31000), hc, app(ty_Maybe, bfg)) → new_esEs5(vuu3000, vuu31000, bfg)
new_esEs23(vuu3000, vuu31000, app(ty_Maybe, cc)) → new_esEs5(vuu3000, vuu31000, cc)
new_esEs8(Left(vuu3000), Left(vuu31000), app(ty_Ratio, bdf), hd) → new_esEs7(vuu3000, vuu31000, bdf)
new_esEs5(Just(vuu3000), Just(vuu31000), app(app(ty_@2, ea), eb)) → new_esEs15(vuu3000, vuu31000, ea, eb)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Bool, hd) → new_esEs11(vuu3000, vuu31000)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Ordering, hd) → new_esEs13(vuu3000, vuu31000)
new_primPlusNat0(Succ(vuu490), vuu3100000) → Succ(Succ(new_primPlusNat1(vuu490, vuu3100000)))
new_esEs8(Left(vuu3000), Left(vuu31000), app(app(ty_@2, bef), beg), hd) → new_esEs15(vuu3000, vuu31000, bef, beg)
new_esEs26(vuu300, vuu3100, app(ty_[], bc)) → new_esEs4(vuu300, vuu3100, bc)
new_span2Ys2(vuu11, vuu12, :(vuu150, vuu151), cf) → new_span2Ys11(vuu11, vuu12, vuu150, vuu151, new_esEs4(:(vuu11, vuu12), vuu150, cf), cf)
new_span2Ys11(vuu11, vuu12, vuu150, vuu151, True, cf) → new_span2Ys12(vuu11, vuu12, vuu150, vuu151, new_span2Ys2(vuu11, vuu12, vuu151, cf), new_span2Zs2(vuu11, vuu12, vuu151, cf), cf)
new_esEs5(Just(vuu3000), Just(vuu31000), app(app(ty_Either, db), dc)) → new_esEs8(vuu3000, vuu31000, db, dc)
new_esEs5(Nothing, Just(vuu31000), cg) → False
new_esEs5(Just(vuu3000), Nothing, cg) → False
new_esEs19(vuu3001, vuu31001, ty_Integer) → new_esEs16(vuu3001, vuu31001)
new_esEs19(vuu3001, vuu31001, ty_Char) → new_esEs6(vuu3001, vuu31001)
new_primEqInt(Neg(Succ(vuu30000)), Neg(Succ(vuu310000))) → new_primEqNat0(vuu30000, vuu310000)
new_esEs4([], [], bc) → True
new_esEs20(vuu3000, vuu31000, ty_Float) → new_esEs17(vuu3000, vuu31000)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_@0, hd) → new_esEs10(vuu3000, vuu31000)
new_esEs18(vuu3000, vuu31000, ty_@0) → new_esEs10(vuu3000, vuu31000)
new_span2Zs2(vuu24, vuu25, [], bb) → []
new_primPlusNat1(Succ(vuu4900), Zero) → Succ(vuu4900)
new_primPlusNat1(Zero, Succ(vuu31000000)) → Succ(vuu31000000)
new_esEs23(vuu3000, vuu31000, app(ty_Ratio, bd)) → new_esEs7(vuu3000, vuu31000, bd)
new_esEs18(vuu3000, vuu31000, app(ty_Ratio, ee)) → new_esEs7(vuu3000, vuu31000, ee)
new_esEs8(Left(vuu3000), Right(vuu31000), hc, hd) → False
new_esEs8(Right(vuu3000), Left(vuu31000), hc, hd) → False
new_esEs8(Right(vuu3000), Right(vuu31000), hc, app(app(ty_Either, bfa), bfb)) → new_esEs8(vuu3000, vuu31000, bfa, bfb)
new_esEs6(Char(vuu3000), Char(vuu31000)) → new_primEqNat0(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, app(app(ty_Either, baa), bab)) → new_esEs8(vuu3000, vuu31000, baa, bab)
new_span2Zs11(vuu24, vuu25, vuu280, vuu281, False, bb) → :(vuu280, vuu281)
new_esEs21(vuu3001, vuu31001, ty_Double) → new_esEs14(vuu3001, vuu31001)
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Float) → new_esEs17(vuu3000, vuu31000)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs18(vuu3000, vuu31000, ty_Float) → new_esEs17(vuu3000, vuu31000)
new_esEs5(Nothing, Nothing, cg) → True
new_groupByZs00(vuu24, vuu25, vuu26, vuu27, vuu28, True, False, bb) → new_groupByZs01(vuu24, vuu25, vuu26, vuu27, vuu28, bb)
new_span2Zs3([], ba) → []
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs18(vuu3000, vuu31000, ty_Bool) → new_esEs11(vuu3000, vuu31000)
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Char) → new_esEs6(vuu3000, vuu31000)
new_esEs22(vuu3002, vuu31002, ty_Integer) → new_esEs16(vuu3002, vuu31002)
new_primEqInt(Neg(Succ(vuu30000)), Neg(Zero)) → False
new_primEqInt(Neg(Zero), Neg(Succ(vuu310000))) → False
new_groupByZs02(vuu24, vuu25, vuu26, vuu27, vuu28, vuu38, bb) → new_span2Zs2(vuu24, vuu25, vuu28, bb)
new_esEs26(vuu300, vuu3100, ty_Char) → new_esEs6(vuu300, vuu3100)
new_esEs23(vuu3000, vuu31000, ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs20(vuu3000, vuu31000, ty_@0) → new_esEs10(vuu3000, vuu31000)
new_esEs4(:(vuu3000, vuu3001), [], bc) → False
new_esEs4([], :(vuu31000, vuu31001), bc) → False
new_span2Zs13(vuu3110, vuu3111, vuu45, vuu44, ba) → vuu44
new_esEs20(vuu3000, vuu31000, ty_Integer) → new_esEs16(vuu3000, vuu31000)
new_esEs22(vuu3002, vuu31002, app(ty_Maybe, bdc)) → new_esEs5(vuu3002, vuu31002, bdc)
new_esEs21(vuu3001, vuu31001, app(ty_Maybe, bca)) → new_esEs5(vuu3001, vuu31001, bca)
new_esEs21(vuu3001, vuu31001, ty_Float) → new_esEs17(vuu3001, vuu31001)
new_primPlusNat1(Zero, Zero) → Zero
new_span2Zs2(vuu24, vuu25, :(vuu280, vuu281), bb) → new_span2Zs11(vuu24, vuu25, vuu280, vuu281, new_esEs4(:(vuu24, vuu25), vuu280, bb), bb)
new_asAs(True, vuu37) → vuu37
new_esEs5(Just(vuu3000), Just(vuu31000), ty_@0) → new_esEs10(vuu3000, vuu31000)
new_primMulNat0(Succ(vuu300000), Succ(vuu3100000)) → new_primPlusNat0(new_primMulNat0(vuu300000, Succ(vuu3100000)), vuu3100000)
new_esEs26(vuu300, vuu3100, ty_Integer) → new_esEs16(vuu300, vuu3100)
new_esEs19(vuu3001, vuu31001, app(ty_[], gc)) → new_esEs4(vuu3001, vuu31001, gc)
new_esEs8(Right(vuu3000), Right(vuu31000), hc, ty_Int) → new_esEs9(vuu3000, vuu31000)
new_esEs18(vuu3000, vuu31000, ty_Double) → new_esEs14(vuu3000, vuu31000)
new_esEs13(LT, LT) → True
new_esEs22(vuu3002, vuu31002, app(ty_[], bcg)) → new_esEs4(vuu3002, vuu31002, bcg)
new_esEs11(False, False) → True
new_span2Ys3(:(vuu3110, vuu3111), ba) → new_span2Ys13(vuu3110, vuu3111, new_esEs4([], vuu3110, ba), ba)
new_primEqInt(Pos(Succ(vuu30000)), Pos(Succ(vuu310000))) → new_primEqNat0(vuu30000, vuu310000)
new_esEs8(Right(vuu3000), Right(vuu31000), hc, ty_Char) → new_esEs6(vuu3000, vuu31000)
new_span2Ys11(vuu11, vuu12, vuu150, vuu151, False, cf) → []
new_esEs8(Right(vuu3000), Right(vuu31000), hc, ty_Float) → new_esEs17(vuu3000, vuu31000)
new_esEs22(vuu3002, vuu31002, app(app(ty_Either, bce), bcf)) → new_esEs8(vuu3002, vuu31002, bce, bcf)
new_esEs19(vuu3001, vuu31001, ty_@0) → new_esEs10(vuu3001, vuu31001)
new_span2Ys3([], ba) → []
new_esEs25(vuu3001, vuu31001, ty_Int) → new_esEs9(vuu3001, vuu31001)
new_groupByZs0([], :([], vuu311), ba) → new_span2Zs3(vuu311, ba)
new_esEs8(Left(vuu3000), Left(vuu31000), ty_Integer, hd) → new_esEs16(vuu3000, vuu31000)
new_esEs8(Left(vuu3000), Left(vuu31000), app(app(app(ty_@3, beb), bec), bed), hd) → new_esEs12(vuu3000, vuu31000, beb, bec, bed)
new_esEs5(Just(vuu3000), Just(vuu31000), ty_Bool) → new_esEs11(vuu3000, vuu31000)
new_primEqNat0(Succ(vuu30000), Succ(vuu310000)) → new_primEqNat0(vuu30000, vuu310000)
new_esEs8(Right(vuu3000), Right(vuu31000), hc, ty_Bool) → new_esEs11(vuu3000, vuu31000)
new_esEs9(vuu300, vuu3100) → new_primEqInt(vuu300, vuu3100)
new_esEs20(vuu3000, vuu31000, ty_Double) → new_esEs14(vuu3000, vuu31000)
new_esEs8(Left(vuu3000), Left(vuu31000), app(ty_Maybe, bee), hd) → new_esEs5(vuu3000, vuu31000, bee)
new_span2Zs3(:(vuu3110, vuu3111), ba) → new_span2Zs12(vuu3110, vuu3111, new_esEs4([], vuu3110, ba), ba)
new_esEs8(Right(vuu3000), Right(vuu31000), hc, app(ty_Ratio, beh)) → new_esEs7(vuu3000, vuu31000, beh)
new_esEs21(vuu3001, vuu31001, app(ty_Ratio, bbb)) → new_esEs7(vuu3001, vuu31001, bbb)
new_esEs23(vuu3000, vuu31000, app(app(ty_@2, cd), ce)) → new_esEs15(vuu3000, vuu31000, cd, ce)
new_esEs26(vuu300, vuu3100, ty_Ordering) → new_esEs13(vuu300, vuu3100)
new_primEqInt(Pos(Zero), Pos(Succ(vuu310000))) → False
new_primEqInt(Pos(Succ(vuu30000)), Pos(Zero)) → False
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_span2Zs11(vuu24, vuu25, vuu280, vuu281, True, bb) → new_span2Zs14(vuu24, vuu25, vuu280, vuu281, new_span2Ys2(vuu24, vuu25, vuu281, bb), new_span2Zs2(vuu24, vuu25, vuu281, bb), bb)
new_esEs23(vuu3000, vuu31000, ty_Ordering) → new_esEs13(vuu3000, vuu31000)
new_esEs23(vuu3000, vuu31000, app(ty_[], bg)) → new_esEs4(vuu3000, vuu31000, bg)
new_esEs21(vuu3001, vuu31001, ty_Char) → new_esEs6(vuu3001, vuu31001)
The set Q consists of the following terms:
new_esEs10(@0, @0)
new_esEs8(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_esEs22(x0, x1, ty_Integer)
new_groupByZs00(x0, x1, x2, x3, x4, False, x5, x6)
new_esEs5(Just(x0), Just(x1), app(ty_Ratio, x2))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_span2Zs12(x0, x1, True, x2)
new_esEs18(x0, x1, ty_Integer)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_span2Ys2(x0, x1, :(x2, x3), x4)
new_esEs8(Left(x0), Left(x1), ty_Int, x2)
new_esEs20(x0, x1, app(ty_Maybe, x2))
new_groupByZs0(:(x0, x1), :([], x2), x3)
new_groupByZs01(x0, x1, x2, x3, x4, x5)
new_esEs11(True, True)
new_esEs5(Just(x0), Just(x1), ty_Float)
new_esEs5(Just(x0), Just(x1), ty_Bool)
new_esEs4([], [], x0)
new_groupByZs02(x0, x1, x2, x3, x4, x5, x6)
new_primEqNat0(Zero, Succ(x0))
new_esEs8(Left(x0), Left(x1), ty_Double, x2)
new_esEs26(x0, x1, ty_Integer)
new_esEs20(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Float)
new_span2Zs11(x0, x1, x2, x3, False, x4)
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs18(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Int)
new_esEs8(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs23(x0, x1, ty_Char)
new_esEs26(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs20(x0, x1, ty_Float)
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs22(x0, x1, ty_@0)
new_groupByZs0(x0, [], x1)
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs5(Just(x0), Just(x1), ty_Integer)
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs20(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs19(x0, x1, app(app(ty_@2, x2), x3))
new_span2Ys3(:(x0, x1), x2)
new_esEs5(Just(x0), Just(x1), ty_Int)
new_esEs13(GT, GT)
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs8(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs21(x0, x1, ty_Integer)
new_span2Zs12(x0, x1, False, x2)
new_span2Ys13(x0, x1, False, x2)
new_esEs18(x0, x1, ty_Bool)
new_esEs15(@2(x0, x1), @2(x2, x3), x4, x5)
new_primEqInt(Neg(Zero), Neg(Zero))
new_span2Ys14(x0, x1, x2, x3, x4)
new_esEs20(x0, x1, ty_Char)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_esEs8(Left(x0), Left(x1), ty_Bool, x2)
new_esEs20(x0, x1, ty_@0)
new_esEs22(x0, x1, ty_Bool)
new_esEs26(x0, x1, app(app(ty_@2, x2), x3))
new_esEs21(x0, x1, ty_Int)
new_esEs5(Just(x0), Nothing, x1)
new_esEs19(x0, x1, ty_Int)
new_esEs8(Right(x0), Right(x1), x2, ty_Int)
new_esEs11(True, False)
new_esEs11(False, True)
new_esEs8(Right(x0), Left(x1), x2, x3)
new_esEs8(Left(x0), Right(x1), x2, x3)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs8(Left(x0), Left(x1), ty_Float, x2)
new_primMulNat0(Succ(x0), Zero)
new_esEs8(Right(x0), Right(x1), x2, ty_Bool)
new_sr(Pos(x0), Pos(x1))
new_esEs6(Char(x0), Char(x1))
new_esEs18(x0, x1, app(app(ty_@2, x2), x3))
new_groupByZs0([], :([], x0), x1)
new_esEs4([], :(x0, x1), x2)
new_esEs26(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_Char)
new_span2Ys2(x0, x1, [], x2)
new_span2Zs2(x0, x1, [], x2)
new_esEs8(Right(x0), Right(x1), x2, ty_Double)
new_esEs5(Just(x0), Just(x1), app(ty_Maybe, x2))
new_esEs19(x0, x1, ty_Ordering)
new_esEs25(x0, x1, ty_Integer)
new_esEs26(x0, x1, ty_Double)
new_esEs18(x0, x1, app(app(ty_Either, x2), x3))
new_esEs5(Nothing, Nothing, x0)
new_sr(Pos(x0), Neg(x1))
new_sr(Neg(x0), Pos(x1))
new_esEs8(Right(x0), Right(x1), x2, ty_@0)
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_esEs8(Left(x0), Left(x1), ty_@0, x2)
new_esEs21(x0, x1, ty_Double)
new_esEs26(x0, x1, ty_Bool)
new_esEs13(GT, LT)
new_esEs13(LT, GT)
new_esEs5(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_span2Zs2(x0, x1, :(x2, x3), x4)
new_span2Ys12(x0, x1, x2, x3, x4, x5, x6)
new_esEs19(x0, x1, ty_Float)
new_esEs18(x0, x1, ty_Float)
new_esEs23(x0, x1, ty_@0)
new_sr(Neg(x0), Neg(x1))
new_esEs5(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs8(Right(x0), Right(x1), x2, ty_Float)
new_esEs26(x0, x1, app(ty_[], x2))
new_primEqNat0(Zero, Zero)
new_esEs8(Right(x0), Right(x1), x2, ty_Integer)
new_esEs14(Double(x0, x1), Double(x2, x3))
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs19(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, ty_@0)
new_esEs8(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs13(GT, EQ)
new_esEs13(EQ, GT)
new_esEs8(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs13(LT, LT)
new_esEs21(x0, x1, ty_Float)
new_esEs19(x0, x1, app(app(ty_Either, x2), x3))
new_span2Zs14(x0, x1, x2, x3, x4, x5, x6)
new_esEs24(x0, x1, ty_Integer)
new_span2Zs3([], x0)
new_primMulNat0(Zero, Zero)
new_span2Ys13(x0, x1, True, x2)
new_span2Ys3([], x0)
new_esEs5(Just(x0), Just(x1), ty_Ordering)
new_esEs8(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs8(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs19(x0, x1, ty_Bool)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs26(x0, x1, app(app(ty_Either, x2), x3))
new_span2Zs13(x0, x1, x2, x3, x4)
new_esEs5(Just(x0), Just(x1), ty_@0)
new_esEs21(x0, x1, ty_Ordering)
new_esEs18(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, ty_Bool)
new_groupByZs0([], :(:(x0, x1), x2), x3)
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs23(x0, x1, ty_Integer)
new_esEs22(x0, x1, ty_Int)
new_esEs19(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs13(LT, EQ)
new_esEs13(EQ, LT)
new_esEs26(x0, x1, app(ty_Maybe, x2))
new_esEs5(Nothing, Just(x0), x1)
new_primEqNat0(Succ(x0), Zero)
new_span2Zs11(x0, x1, x2, x3, True, x4)
new_esEs19(x0, x1, ty_@0)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_span2Ys11(x0, x1, x2, x3, False, x4)
new_esEs13(EQ, EQ)
new_esEs23(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Double)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs7(:%(x0, x1), :%(x2, x3), x4)
new_esEs26(x0, x1, ty_Float)
new_esEs21(x0, x1, ty_Bool)
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs26(x0, x1, ty_Ordering)
new_primMulNat0(Succ(x0), Succ(x1))
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_asAs(True, x0)
new_esEs8(Left(x0), Left(x1), app(ty_[], x2), x3)
new_esEs18(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Zero, Succ(x0))
new_esEs19(x0, x1, ty_Double)
new_primPlusNat1(Succ(x0), Zero)
new_esEs8(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs26(x0, x1, ty_@0)
new_esEs8(Right(x0), Right(x1), x2, ty_Char)
new_esEs23(x0, x1, ty_Double)
new_esEs8(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs4(:(x0, x1), [], x2)
new_esEs4(:(x0, x1), :(x2, x3), x4)
new_esEs5(Just(x0), Just(x1), ty_Char)
new_esEs5(Just(x0), Just(x1), app(ty_[], x2))
new_esEs11(False, False)
new_esEs20(x0, x1, app(ty_Ratio, x2))
new_esEs8(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs20(x0, x1, ty_Bool)
new_esEs22(x0, x1, ty_Ordering)
new_esEs22(x0, x1, ty_Char)
new_esEs17(Float(x0, x1), Float(x2, x3))
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs18(x0, x1, ty_@0)
new_groupByZs00(x0, x1, x2, x3, x4, True, False, x5)
new_groupByZs0(:(x0, x1), :(:(x2, x3), x4), x5)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs19(x0, x1, ty_Char)
new_esEs19(x0, x1, app(ty_[], x2))
new_esEs8(Left(x0), Left(x1), ty_Char, x2)
new_esEs16(Integer(x0), Integer(x1))
new_primMulNat0(Zero, Succ(x0))
new_esEs20(x0, x1, ty_Double)
new_span2Zs3(:(x0, x1), x2)
new_primPlusNat1(Zero, Zero)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs23(x0, x1, ty_Float)
new_span2Ys11(x0, x1, x2, x3, True, x4)
new_primPlusNat0(Succ(x0), x1)
new_esEs18(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_groupByZs00(x0, x1, x2, x3, x4, True, True, x5)
new_esEs8(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs18(x0, x1, ty_Int)
new_asAs(False, x0)
new_esEs18(x0, x1, app(ty_[], x2))
new_esEs20(x0, x1, app(ty_[], x2))
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs23(x0, x1, ty_Int)
new_esEs26(x0, x1, ty_Char)
new_esEs18(x0, x1, ty_Char)
new_esEs5(Just(x0), Just(x1), ty_Double)
new_primPlusNat0(Zero, x0)
new_esEs20(x0, x1, ty_Ordering)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs8(Right(x0), Right(x1), x2, app(ty_[], x3))
new_esEs5(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs12(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs20(x0, x1, app(app(ty_@2, x2), x3))
new_esEs9(x0, x1)
new_esEs25(x0, x1, ty_Int)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs8(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs18(x0, x1, ty_Ordering)
new_esEs20(x0, x1, ty_Int)
new_esEs19(x0, x1, ty_Integer)
new_esEs24(x0, x1, ty_Int)
new_esEs20(x0, x1, app(app(ty_Either, x2), x3))
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs19(x0, x1, app(ty_Maybe, x2))
new_esEs8(Left(x0), Left(x1), ty_Integer, x2)
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.